formal-mathfin: A Formally Verified Library of Mathematical Finance in Lean 4
A Lean 4 library of machine-checked mathematical-finance theorems: 535 sorry-free theorems, 522 of them delivery-ready, depending only on the axioms propext, Classical.choice and Quot.sound. It covers continuous-time stochastic calculus (the Ito integral, Ito's formula, quadratic variation and martingale representation...