Formalizing Automated Market Makers in the Lean 4 Theorem Prover

Daniele Pusceddu, Massimo Bartoletti

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 a…