formal-applied-math/formal-mathfin

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

View on GitHub
Lean
Stars 36
Forks 12
License Apache-2.0
Open Issues 141
Updated 8m ago