A Formal Approach to AMM Fee Mechanisms with Lean 4

TL;DR

The paper addresses modeling Automated Market Makers (AMMs) with trading fees in a formal, machine-checked Lean 4 setting. It introduces the fee-adjusted constant-product swap rate $SX_{\phi} = \frac{\phi r_1}{r_0 + \phi x}$ and analyzes how fees affect economic properties, showing that output-boundedness and monotonicity hold while additivity becomes generalized and a single large swap can outperform splitting. It derives a closed-form, unique arbitrage solution and proves a separation between the equilibrium value that aligns internal and external prices and the actual profit-maximizing swap, supported by formal Lean 4 proofs (Lean 4 extension with roughly 3500 lines). The work contributes high-assurance reasoning about fee effects in CPMMs, informs real-world AMM design (e.g., Uniswap v2-like behavior), and lays groundwork for future analyses of MEV and advanced fee structures.

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 $φ\in(0,1]$, into the swap rate function. Fee amounts increase inversely proportional to $φ$. When $φ= 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 $φ< 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.

Figures (2)

• Figure 1: $\mathit{G}_{{\color{ForestGreen}{\sf{A}}}_{\color{ForestGreen}{{}}}\xspace}( {{\color{MidnightBlue}{\sf T}}_{\color{MidnightBlue}{}}(x)})$
• Figure 2: $\mathit{G}_{{\color{ForestGreen}{\sf{A}}}_{\color{ForestGreen}{{}}}\xspace}( {{\color{MidnightBlue}{\sf T}}_{\color{MidnightBlue}{}}(x)})$ zoomed.

Theorems & Definitions (14)

• Example 1
• Example 2
• Example 3
• Lemma 4
• Lemma 5
• Lemma 6: Additivity of swap rate
• Example 7
• Theorem 8: Additivity of swap gain
• Theorem 9: Equilibrium value
• Lemma 10: Uniqueness of equilibrium swap value