Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2602.00101

A Formal Approach to AMM Fee Mechanisms with Lean 4

Marco Dessalvi·Massimo Bartoletti·Alberto Lluch-Lafuente
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

q-fin.MFcs.CEcs.CRq-fin.TR

Keep this discovery

BibTeXRIS

Marco Dessalvi, Massimo Bartoletti, Alberto Lluch-Lafuente. 2026-01-24. A Formal Approach to AMM Fee Mechanisms with Lean 4. https://arxiv.org/abs/2602.00101

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Variance-Optimal Hedging in the Rough Hawkes--Heston Model

We study variance-optimal stock hedging and the convergence of approximate strategies in the rough Hawkes--Heston model. Starting from the model's affine conditional transform and the affine Volterra jump framework, we obtain semi-explicit hedges for European calls and a representation of the minimum quadratic error through the Galtchouk--Kunita--Watanabe projection. Our main approximation result keeps the original stock, variance driver, and information flow fixed while regularizing the kernel used to evaluate the hedge. To handle singular memory and common marked jumps, we construct the approximate holdings from histories available before trading and preserve the conditional transform's random modulus envelope. Riccati--Volterra stability and weighted truncation then yield convergence in the original stock's trading norm on compact Fourier intervals. For calls, a joint choice of kernel regularization and Fourier cutoff gives convergence of the initial capitals and strategies, uniform-in-time square-mean convergence of continuous-time gains, and convergence of the terminal mean-square error to the variance-optimal value. A numerical experiment with shifted fractional kernels illustrates the construction on common original-market paths.

q-fin.MF↗
arXiv2026

Numeraire Invariance of Entropy-Projected Martingale Measures

Let \(P\) be a fixed physical law and let \(Q\) be an equivalent martingale measure selected from the martingale-measure set associated with a chosen numeraire. A change of numeraire maps \(Q\) to \(T_LQ\), where \(d(T_LQ)=L\,dQ\) and \(L\) is the terminal likelihood ratio. The forward relative-entropy projection minimizing \(D_{\mathrm{KL}}(P\Vert Q)\) commutes with this transform because its objective changes only by the constant \(-E_P\log L\). The minimal entropy martingale measure (MEMM) orientation \(D_{\mathrm{KL}}(Q\Vert P)\) does not have this property, and a trinomial counterexample shows that independently recomputed MEMMs need not be likelihood compatible. We make two economic consequences explicit. First, the two entropy orientations are precisely the \(Q\)-dependent terms in the classical convex-dual objectives for logarithmic and exponential utility, respectively. Second, likelihood compatibility is equivalent to equality of the pricing functionals obtained in the two numeraires. Hence the forward selectors value every integrable claim consistently across numeraires, whereas the two MEMMs in the counterexample assign different prices to a nonreplicable digital claim. We also prove a finite-state class-level characterization: uniform invariance over the elementary one-period likelihood-ratio families forces a smooth convex \(f\)-divergence to be logarithmic, up to scaling and affine equivalence. Finally, in finite-state markets, the forward projection exists under the usual strictly positive feasible-point condition; its density \(dP/dQ^*\) is attainable log-optimal terminal wealth, and the minimum forward entropy equals maximal expected log growth.

q-fin.MF↗
arXiv2026

The Delta of a Variance Swap

We define the variance swap delta as the sensitivity of the price of variance to a change in underlying price. We use Carr-Madan spanning formulas to analyze this sensitivity when the implied volatility smile curve may depend on the underlying price. We show that the variance swap total delta is zero for the class of smile curves that are pure functions of (log) moneyness, which goes against the empirical observation that variance is up when the market is down. We propose a simple modification of the smile to correct this issue.

q-fin.MF↗