Reproduce “A Formal Approach to AMM Fee Mechanisms with Lean 4” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Marco Dessalvi, Massimo Bartoletti, Alberto Lluch-Lafuente
This research formally integrates trading fees into Constant-Product Market Maker models, leveraging Lean 4 for machine-checked analysis. It establishes that split swaps are suboptimal for traders and derives distinct closed-form solutions for market equilibrium and maximum arbitrage profit in fee-adjusted AMMs.
Key insights
- Trading fees fundamentally alter the additivity property of AMM swap functions, causing a single large swap to yield greater gain than multiple split swaps for a trader.
- In fee-adjusted AMMs, the swap amount that brings the market to equilibrium (aligning internal and external rates) is generally distinct from and suboptimal for maximizing an arbitrageur's profit.
- Core structural properties of Constant-Product Market Makers, such as output-boundedness and strict monotonicity, are preserved even when trading fees are incorporated into the model.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.