Formalizing Automated Market Makers in the Lean 4 Theorem Prover. - Daniele Pusceddu; Massimo Bartoletti (FMBC@CAV, 2024)