在 Lean 4 定理证明器中形式化自动做市商
计算机科学中的逻辑
2024-02-13 v1 计算工程、金融与科学
计算机科学与博弈论
摘要
自动做市商（AMMs）是去中心化金融（DeFi）生态系统的重要组成部分，因为它们允许用户无需受信任的权威机构或外部价格预言机即可交换加密资产。尽管这些协议基于相对简单的机制（例如算法确定加密资产之间的汇率），但它们引发了复杂的经济行为。研究其结构和经济属性的模型激增证明了这种复杂性。目前，在这些模型上获得的大多数理论结果都由手工证明支持。本工作提出了在 Lean 4 定理证明器中对恒定乘积 AMM 的形式化。为了展示我们模型的实用性，我们提供了关键经济属性（如套利）的机械化证明，据我们所知，这些属性此前仅通过手工证明得以证实。
引用
@article{arxiv.2402.06064,
title = {Formalizing Automated Market Makers in the Lean 4 Theorem Prover},
author = {Daniele Pusceddu and Massimo Bartoletti},
journal= {arXiv preprint arXiv:2402.06064},
year = {2024}
}