标题： 一种使用 Lean 4 的 AMM 费用机制的形式化方法 显示英文标题

标题： A Formal Approach to AMM Fee Mechanisms with Lean 4

摘要： 去中心化金融（DeFi）通过在没有可信中介的情况下实现复杂的资产交换协议，彻底改变了金融市场。 自动做市商（AMMs）是DeFi的核心组成部分，提供了在算法计算的汇率下不同类型的资产交换的核心功能。 几种主流的AMM实现基于恒定乘积模型，该模型确保交换保持AMM中代币储备的乘积——除了一个用于激励流动性提供的\emph{交易费用}。 交易费用显著地复杂化了AMMs的经济特性，因此一些AMM模型会忽略它们以简化分析。 然而，交易费用对用户的交易策略有非微小的影响，因此开发精确考虑其影响的精细AMM模型至关重要。 我们通过在交换率函数中引入一个新的参数，即交易费用$φ\in(0,1]$，扩展了一个基础的AMM模型。 费用金额与$φ$成反比增加。 当$φ= 1$时，不收取费用，恢复原始模型。 我们从经济角度分析了由此产生的费用调整模型。 我们证明了交换率函数的几个关键属性，包括输出有界性和单调性，仍然得到保留。 同时，其他属性——最明显的是可加性——不再成立。 我们通过推导出一种广义的可加性形式来精确描述这种偏差，该形式捕捉了在存在交易费用的情况下交换的影响。 我们证明了当$φ< 1$时，执行一次大的交换比将交易拆分为较小的交易获得更高的利润。 最后，我们在存在交易费用的情况下推导出套利问题的闭式解，并证明其唯一性。 所有结果都在Lean 4证明助手中进行了形式化和机器验证。 显示英文摘要

摘要： 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.