A Formal Approach to AMM Fee Mechanisms with Lean 4

TL;DR

This paper introduces a formal, fee-adjusted model for Automated Market Makers in DeFi, analyzing its properties, economic implications, and providing a verified solution for arbitrage, all formalized in Lean 4.

Contribution

It extends foundational AMM models by incorporating trading fees, analyzes their impact on properties and strategies, and formalizes the results in Lean 4.

Findings

Key properties like output-boundedness are preserved with fees

Executing large trades yields more profit than splitting into smaller trades when fees are present

A unique, closed-form arbitrage solution is derived and verified in Lean 4

Abstract

Decentralized Finance (DeFi) has revolutionized financial markets by enabling complex asset-exchange protocols without trusted intermediaries. Automated Market Makers (AMMs) are a central component of DeFi, providing the core functionality of swapping assets of different types at algorithmically computed exchange rates. Several mainstream AMM implementations are based on the constant-product model, which ensures that swaps preserve the product of the token reserves in the AMM -- up to a \emph{trading fee} used to incentivize liquidity provision. Trading fees substantially complicate the economic properties of AMMs, and for this reason some AMM models abstract them away in order to simplify the analysis. However, trading fees have a non-trivial impact on users' trading strategies, making it crucial to develop refined AMM models that precisely account for their effects. We extend a foundational model of AMMs by introducing a new parameter, the trading fee $\phi\in(0,1]$, into the swap rate function. Fee amounts increase inversely proportional to $\phi$. When $\phi = 1$, no fee is applied and the original model is recovered. We analyze the resulting fee-adjusted model from an economic perspective. We show that several key properties of the swap rate function, including output-boundedness and monotonicity, are preserved. At the same time, other properties - most notably additivity - no longer hold. We precisely characterize this deviation by deriving a generalized form of additivity that captures the effect of swaps in the presence of trading fees. We prove that when $\phi < 1$, executing a single large swap yields strictly greater profit than splitting the trade into smaller ones. Finally, we derive a closed-form solution to the arbitrage problem in the presence of trading fees and prove its uniqueness. All results are formalized and machine-checked in the Lean 4 proof assistant.