{"repo":"formal-applied-math/formal-mathfin","free":true,"listed":false,"github":"https://github.com/formal-applied-math/formal-mathfin","clone":"git clone https://github.com/formal-applied-math/formal-mathfin.git","description":"Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.","language":"Lean","stars":30,"topics":["black-scholes","formal-verification","lean4","mathlib","option-pricing","quantitative-finance","theorem-proving","derivatives-pricing","formal-methods","ito-calculus"],"license":"Apache-2.0","category":"trading","readme_excerpt":"Mathematical finance, formally verified A Lean 4 library building toward a formal theory of mathematical finance — every result machine-checked against Mathlib and Degenne's BrownianMotion, with an exact statement of what is proved and what is assumed, and the deep connections between the field's pillars made load-bearing rather than decorative. 353 theorems · 340 delivery-ready · 0 sorries · axioms-clean · lake build is the proof. --- What we're building Formalized finance is usually a scattering of isolated results. The ambition here is a theory : prove the Black–Scholes world, the Itô tower, the Fundamental Theorem of Asset Pricing, and the risk-measure layer — then wire them together around the field's actual organizing principles, so that the architecture is the artifact, not just the catalogue. \"Top-notch\" here is not more theorems — it is the theorems organized around the field's spine, with the deep cross-connections proved. Two commitments make that trustworthy: - The build is the proof. A clean lake build re-elaborates every theorem against pinned Lean + Mathlib. There is no sorry and no project-local axiom anywhere; every full result depends only on the three standard axioms propext, Classical.choice, Quot.sound , #print axioms -pinned as a CI invariant in MathFin/AxiomAudit.lean . - Honest scope, enforced — never overclaimed. Every entry declares a faithfulness status ( full / library wrapper / reduced core ); an input-hash verification ledger records exactly what","default_branch":null,"files":null,"tree":[],"storefront":"/r/formal-applied-math","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/formal-applied-math/formal-mathfin/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}