A Formal Approach to AMM Fee Mechanisms with Lean 4

• URL: http://arxiv.org/abs/2602.00101v1
• Date: Sat, 24 Jan 2026 20:47:42 GMT
• Title: A Formal Approach to AMM Fee Mechanisms with Lean 4
• Authors: Marco Dessalvi, Massimo Bartoletti, Alberto Lluch-Lafuente,
• Abstract summary: Automated Market Makers (AMMs) are a central component of DeFi.<n> trading fees substantially complicate the economic properties of AMMs.<n>We show that several key properties of the swap rate function, including output-boundedness and monotonicity, are preserved.
• Score: 0.29858597335303283
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Deep g-Pricing for CSI 300 Index Options with Volatility Trajectories and Market Sentiment [14.215333503141101]
  This paper extends the Black--Scholes--Merton (BSM) model by learning a nonlinear generator within a deep Forward--Backward Differential Equation framework.<n>We propose a dual-network architecture where the value network $u_$ learns option prices and the generator network $g_$ characterizes the pricing mechanism.<n> Empirical results on CSI 300 index options show that our method reduces Mean Absolute Error (MAE) by 32.2% and Mean Absolute Percentage Error (MAPE) by 35.3% compared with BSM.
  arXiv  Detail & Related papers  (2026-01-15T08:58:09Z)
• Robust Reinforcement Learning in Finance: Modeling Market Impact with Elliptic Uncertainty Sets [57.179679246370114]
  In financial applications, reinforcement learning (RL) agents are commonly trained on historical data, where their actions do not influence prices.<n>During deployment, these agents trade in live markets where their own transactions can shift asset prices, a phenomenon known as market impact.<n>Traditional robust RL approaches address this model misspecification by optimizing the worst-case performance over a set of uncertainties.<n>We develop a novel class of elliptic uncertainty sets, enabling efficient and tractable robust policy evaluation.
  arXiv  Detail & Related papers  (2025-10-22T18:22:25Z)
• Trade in Minutes! Rationality-Driven Agentic System for Quantitative Financial Trading [57.28635022507172]
  TiMi is a rationality-driven multi-agent system that architecturally decouples strategy development from minute-level deployment.<n>We propose a two-tier analytical paradigm from macro patterns to micro customization, layered programming design for trading bot implementation, and closed-loop optimization driven by mathematical reflection.
  arXiv  Detail & Related papers  (2025-10-06T13:08:55Z)
• When Priority Fails: Revert-Based MEV on Fast-Finality Rollups [0.0]
  We study the economics of transaction reverts on rollups and show that they are not accidental failures but equilibrium outcomes of MEV strategies.<n>We find that over 80% of reverted transactions are swaps, with half targeting USDC-WETH pools on Uniswap v3, v4.<n>Our findings establish reverts as a structural feature of rollup MEV microstructure and highlight the need for protocol-level reforms to sequencing, fee markets, and revert protection.
  arXiv  Detail & Related papers  (2025-06-02T09:18:53Z)
• STORM: A Spatio-Temporal Factor Model Based on Dual Vector Quantized Variational Autoencoders for Financial Trading [55.02735046724146]
  In financial trading, factor models are widely used to price assets and capture excess returns from mispricing.<n>We propose a Spatio-Temporal factOR Model based on dual vector quantized variational autoencoders, named STORM.<n>Storm extracts features of stocks from temporal and spatial perspectives, then fuses and aligns these features at the fine-grained and semantic level, and represents the factors as multi-dimensional embeddings.
  arXiv  Detail & Related papers  (2024-12-12T17:15:49Z)
• RediSwap: MEV Redistribution Mechanism for CFMMs [6.475701705193783]
  We introduce RediSwap, a novel AMM designed to capture Maximal Extractable Value (MEV) at the application level and refund it fairly among users and liquidity providers. At its core, RediSwap features an MEV-redistribution mechanism that manages arbitrage opportunities within the AMM pool. We prove that our mechanism is incentive-compatible and Sybil-proof, and demonstrate that it is easy for arbitrageurs to participate.
  arXiv  Detail & Related papers  (2024-10-24T05:11:41Z)
• Uniswap Liquidity Provision: An Online Learning Approach [49.145538162253594]
  Decentralized Exchanges (DEXs) are new types of marketplaces leveraging technology. One such DEX, Uniswap v3, allows liquidity providers to allocate funds more efficiently by specifying an active price interval for their funds. This introduces the problem of finding an optimal strategy for choosing price intervals. We formalize this problem as an online learning problem with non-stochastic rewards.
  arXiv  Detail & Related papers  (2023-02-01T17:21:40Z)
• QLAMMP: A Q-Learning Agent for Optimizing Fees on Automated Market Making Protocols [5.672898304129217]
  We develop a Q-Learning Agent for Market Making Protocols (QLAMMP) that learns the optimal fee rates and leverage coefficients for a given AMM protocol. We show that QLAMMP is consistently able to outperform its static counterparts under all the simulated test conditions.
  arXiv  Detail & Related papers  (2022-11-28T00:30:45Z)
• Benefits of Permutation-Equivariance in Auction Mechanisms [90.42990121652956]
  An auction mechanism that maximizes the auctioneer's revenue while minimizes bidders' ex-post regret is an important yet intricate problem in economics. Remarkable progress has been achieved through learning the optimal auction mechanism by neural networks.
  arXiv  Detail & Related papers  (2022-10-11T16:13:25Z)
• Predicting Status of Pre and Post M&A Deals Using Machine Learning and Deep Learning Techniques [0.0]
  Risk arbitrage or merger arbitrage is an investment strategy that speculates on the success of M&A deals. Prediction of the deal status in advance is of great importance for risk arbitrageurs. We present an ML and DL based methodology for takeover success prediction problem.
  arXiv  Detail & Related papers  (2021-08-05T21:26:45Z)
• Weighted QMIX: Expanding Monotonic Value Function Factorisation for Deep Multi-Agent Reinforcement Learning [66.94149388181343]
  We present a new version of a popular $Q$-learning algorithm for MARL. We show that it can recover the optimal policy even with access to $Q*$. We also demonstrate improved performance on predator-prey and challenging multi-agent StarCraft benchmark tasks.
  arXiv  Detail & Related papers  (2020-06-18T18:34:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.