 A Formally Verified Library of Mathematical Finance in Lean 4Raphael Coelho Abstract: We describe a library of mathematical finance built in the Lean~4 proof assistant, on top of Mathlib and the \lean{BrownianMotion} package. It is broad: more than two hundred \lean{sorry}-free theorems across eleven areas, from the measure-theoretic foundations of continuous-time stochastic calculus through derivative pricing to applied risk, portfolio, and fixed-income theory, and, to our knowledge, the most comprehensive machine-checked development of mathematical finance to date. Two things make it more than a catalogue. It reaches into the continuous theory far enough to construct the $L^2$ It\^o integral as a bounded linear isometry and to \emph{derive}, rather than assume, the risk-neutral pricing measure. And it audits its own faithfulness: every result is classified by how its Lean statement relates to the mathematics it claims, and a build-enforced gate pins the axioms each proof actually uses, so a reader can see precisely what has been proved and what has only been proved under added hypotheses. We close with a finding: a formal base over classical financial mathematics yields certified \emph{unification} of known results rather than new financial theory. The contribution is therefore methodological and infrastructural (reusable verified foundations for mathematical finance, together with the faithfulness audit above), not a new financial result. Date: 2026-05, Revised 2026-06 Downloads: (external link) Related works: Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text Persistent link: https://EconPapers.repec.org/RePEc:arx:papers:2606.01356 Access Statistics for this paper More papers in Papers from arXiv.org |
Is your work missing from RePEc? Here is how to contribute.
Questions or problems? Check the EconPapers FAQ or send mail to .
EconPapers is hosted by the
School of Business at Örebro University.