Automated Market Makers (AMMs) are an integral component of the decentralized finance (DeFi) ecosystem, as they allow users to exchange crypto-assets without the need for trusted authorities or external price oracles. Although these protocols are based on relatively simple mechanisms, e.g., to algorithmically determine the exchange rate between crypto-assets, they give rise to complex economic behaviours. This complexity is witnessed by the proliferation of models that study their structural and economic properties. Currently, most of theoretical results obtained on these models are supported by pen-and-paper proofs. This work proposes a formalization of constant-product AMMs in the Lean 4 Theorem Prover. To demonstrate the utility of our model, we provide mechanized proofs of key economic properties like arbitrage, that at the best of our knowledge have only been proved by pen-and-paper before.

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