Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper presents a comprehensive library of mathematical finance developed in the Lean 4 proof assistant, encompassing over two hundred verified theorems across various domains such as stochastic calculus and derivative pricing. The library not only constructs foundational elements like the L2 Itô integral and derives the risk-neutral pricing measure but also includes a rigorous auditing system that classifies the relationship between Lean statements and their mathematical claims. The authors conclude that while the library does not yield new financial theories, it provides a robust methodological framework and reusable verified foundations for future research in mathematical finance.
A comprehensive library of verified mathematical finance theorems reveals the limitations of classical financial mathematics while establishing a rigorous framework for future developments.
We describe a library of mathematical finance built in the Lean 4 proof assistant, on top of Mathlib and the BrownianMotion package. It is broad: more than two hundred 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. Breadth is the setting, not the point. Two things make it more than a catalogue. It reaches into the continuous theory far enough to construct the L2 It\^o integral as a bounded linear isometry and to 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 candid finding: a formal base over classical financial mathematics yields certified 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.