A Formal Approach to AMM Fee Mechanisms with Lean 4

Paper: arXiv 2602.00101

Authors: Marco Dessalvi, Massimo Bartoletti, Alberto Lluch-Lafuente

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.

Complexity vs Empirical Score

• Math Complexity: 8.0/10
• Empirical Rigor: 2.0/10
• Quadrant: Lab Rats — theoretically deep, empirically untested

Why this score: This paper provides a rigorous formal verification of AMM fee mechanisms using the Lean 4 proof assistant, delivering closed-form solutions for arbitrage maximization. While theoretical and mathematical rigor are outstanding, empirical backtesting against real-world DEX market data is absent.

Research Flowchart

  flowchart TD
    A[Research Goal: Formally model AMM trading fees & properties in Lean 4] --> B[Input: Extended Constant-Product Model with Fee Parameter φ ∈ 0,1]
    B --> C[Methodology: Formalization & Machine-Checked Proofs in Lean 4 Assistant]
    C --> D[Economic & Structural Analysis of Swap Rate Function]
    C --> E[Arbitrage Optimization with Fees]
    D --> F[Outcome 1: Preserved Monotonicity & Boundedness; Lost Additivity]
    D --> G[Outcome 2: Proved Single Large Swaps Outperform Split Trades for φ < 1]
    E --> H[Outcome 3: Derived & Proved Unique Closed-Form Arbitrage Solution]

Cited References (249)

1. A Formal Approach to AMM Fee Mechanisms with Lean 4 — → 2602.00101
2. Netting-based Liquidity-saving Automated Market Makers (2025) — link
3. A theory of Automated Market Makers in DeFi (2022) — link
4. Maximizing Extractable Value from Automated Market Makers (2022) — link
5. A Theory of Automated Market Makers in DeFi (2021) — link
6. Towards a Theory of Decentralized Finance (2021) — link
7. The Lean 4 Theorem Prover and Programming Language (2021) — link
8. SoK : Mitigation of Front-running in Decentralized Finance (2021)

3 of 249 cited works are in the corpus; resolved via arXiv source bundles, Semantic Scholar and OpenAlex. Corpus-wide: 2518 linked papers.