raphaelrrcoelho

raphaelrrcoelho/formal-mathfin

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

19 stars 4 forks 19 watchers Lean Apache License 2.0

black-scholes derivatives-pricing formal-methods formal-verification ito-calculus lean4 mathematical-finance mathlib option-pricing quantitative-finance stochastic-calculus theorem-proving

34 Open Issues Need Help Last updated: Jul 1, 2026

Open Issues Need Help

View All on GitHub

Girsanov: derive the continuous EMM from the Itô tower (the I↔II bridge; retire the Wald shortcut) about 13 hours ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Document a Mathlib/toolchain bump cadence policy 2 days ago

documentation help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Itô formula: lower the smoothness hypothesis from C³ to C² (the textbook scope) 2 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Bundle IsBrownianMotion + drop the 4 dead `_hBmeas` args (clear the nolints baseline's genuine slop) 2 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Superhedging strong duality: the EMM-sup equality (needs finite-dim Farkas / polyhedral-cone closedness) 2 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Move off the rc toolchain to stable + document a Mathlib bump cadence 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add SECURITY.md (reporting policy + dependency-pinning trust boundary) 16 days ago

documentation good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add SUPPORT.md with Zulip / communication channels for contributors 16 days ago

documentation good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Generate and host doc-gen4 API documentation on GitHub Pages 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Publish a hosted leanblueprint site with interactive dependency graph 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add Black-76 caplet / floorlet pricing 16 days ago

enhancement good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add a perpetual American option closed form 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

CRR → Black–Scholes convergence rate: explicit error constant 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Variable-coefficient Feynman–Kac: local-vol / Heston PDE on the SDE layer 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Upgrade reduced_core: compound-Poisson MGF → Cramér–Lundberg ruin core 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Upgrade reduced_core: Poisson interarrivals iid Exp (pp-prop-3.3.6) 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Markov cluster: renewal + Perron–Frobenius spectral layer 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Itô formula: lift bounded-derivative scope to unrestricted C² (Summit C localization) 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Itô tower: general-integrand pathwise modification → localized integral 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Upstream: Real.erf / erfc / erfinv for Mathlib 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Depth track: Carr–Lee moment formula (wing-decay bound on E[S_T^p]) 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Depth track: Carr–Madan static replication integral identity 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Depth track: optimal-stopping characterisation of the Snell envelope 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Depth track: discrete-time martingale representation in the binomial model 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Depth track: variance-optimal hedging in finite-state markets 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add a stdlib generator for a repo-level formalization.yaml manifest 16 days ago

enhancement help wanted

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add a CONTRIBUTING/Code-of-Conduct badge row and "Contributing" section to the README 16 days ago

documentation good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Audit MathFin/ module files for the `## Result` docstring section 16 days ago

documentation good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Cross-link every docs/coverage.md entry to its Lean source file 16 days ago

documentation good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Formalize the Black–Scholes third-order Greek "speed" (∂³V/∂S³) 16 days ago

enhancement good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Formalize the Black–Scholes higher-order Greek "charm" (∂Δ/∂τ) 16 days ago

enhancement good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Expand MathFin/Examples.lean into a guided tour for newcomers 16 days ago

documentation good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Write a build & environment troubleshooting FAQ 16 days ago

documentation good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving

Add a glossary mapping finance terms to their Lean definitions 16 days ago

documentation good first issue

raphaelrrcoelho/formal-mathfin

19

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

Lean

#black-scholes#derivatives-pricing#formal-methods#formal-verification#ito-calculus#lean4#mathematical-finance#mathlib#option-pricing#quantitative-finance#stochastic-calculus#theorem-proving