Formalizing Automated Market Makers in the Lean 4 Theorem Prover

自动做市商（AMMs）是去中心化金融（DeFi）生态系统的重要组成部分，因为它们允许用户在不需要信任的权威或外部价格预言机的情况下交换加密资产。尽管这些协议基于相对简单的机制（例如，通过算法确定加密资产之间的汇率），但它们引发了复杂的经济行为。这种复杂性可以通过研究它们的结构和经济属性的模型的增加来证明。目前，这些模型获得的大部分理论结果都是通过纸笔证明支持的。本研究提出了在Lean 4定理证明器中对恒定产品AMMs进行形式化。为了展示我们模型的实用性，我们提供了关键经济属性（如套利）的机械化证明，这些证明在我们所知道的情况下仅通过纸笔证明。

论文旨在在Lean 4定理证明器中形式化常数乘积AMM模型，并提供机械化证明其关键经济属性，例如套利。

通过在Lean 4定理证明器中形式化常数乘积AMM模型，可以提供机械化证明关键经济属性的证明，这在之前只能通过纸笔证明。

该论文提供了机械化证明常数乘积AMM模型的关键经济属性，如套利。实验使用了Lean 4定理证明器，但未使用任何数据集或开源代码。这项工作为进一步研究提供了基础。

在这个领域中，最近的相关研究包括“Automated Market Makers: A Survey”和“Flash Boys 2.0: Frontrunning, Transaction Reordering, and Consensus Instability in Decentralized Exchanges”。