Source-linked AI summary
A Formally Verified Library of Mathematical Finance in Lean 4
Raphael Coelho
TL;DR
Mathematical finance has been scarcely formalized despite substantial theorem-proving foundations. This paper builds a broad Lean 4 library with a constructed continuous Itô integral, a derived risk-neutral measure, and a faithfulness audit, reporting certified unification of classical results rather than new financial theory.
Problem
Almost none of mathematical finance had been formalized despite existing measure-theoretic probability and continuous-time stochastic-process foundations.
Method
The library constructs the continuous L^2 Itô integral, derives risk-neutral measures, and machine-checks each theorem’s statement classification and axiomatic dependencies.
Results
316 of 330 delivery-claim-ready results are reported, with reduced-core items concentrated in continuous-time and discrete-process benchmarks.
Takeaways & Limitations
Formalizing classical financial mathematics yields certified unification and verified infrastructure for reuse, rather than new financial theory.
Takeaways & Limitations
The general multi-period risk-neutral-measure case remains an open rung, while partial cores cluster at the continuous-time frontier.
Abstract
from arXiv · showhide
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 three 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. To our knowledge it is 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ô 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 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 above), not a new financial result.
1 Introduction
The paper presents a broad Lean 4 library of mathematical finance spanning eleven areas, extending prior narrow formalizations into continuous-time stochastic calculus and derivative pricing. Its contribution is methodological: constructing the continuous Itô integral and making each formalization’s mathematical faithfulness machine-checkable, rather than introducing new financial theory.
- Scope: Eleven areas organize the library, from measure-theoretic continuous-time stochastic calculus through pricing, risk, portfolio, and fixed-income theory.The development is built on Mathlib’s probability foundations and the BrownianMotion package.
- Related work: Prior formalizations cover isolated settings, including discrete CRR markets, constant-product automated market makers, and a focused Itô-to-Black–Scholes development.The prior work leaves the continuous Itô integral structurally verified rather than constructed.
- Continuous-time foundations: The stochastic-calculus foundations include Brownian-motion martingales, Wiener and Itô L2 isometries, quadratic variation, a continuous Itô integral, an L2 Itô formula, and a Feynman–Kac link.The Itô formula covers C3 functions and includes a two-dimensional case.
- Financial foundations: The finance foundations add no-arbitrage results including the fundamental theorem of asset pricing, state prices, pricing kernels, convex pricing functionals, and static Girsanov.These foundations support Black–Scholes, binomial, and other option-pricing developments.
- Contribution: The contribution has two axes: constructing the continuous Itô integral and making each formalization’s faithfulness machine-checkable through audited statements.The audit can certify when independently built modules denote the same mathematics.
2 Contributions
The library formalizes mathematical finance broadly and deeply on one coherent Lean 4 foundation, while auditing how faithfully its theorems represent mathematics. Its main technical advances include constructing the continuous L^2 Itô integral, deriving risk-neutral pricing, and machine-checking the binomial-to-Black–Scholes limit.
- Scope: Eleven areas and more than three hundred sorry-free theorems form a coherent, reusable formalization of mathematical finance.The authors describe it as, to their knowledge, the broadest formalization in any proof assistant, measured by breadth.
- Faithfulness audit: The faithfulness audit classifies every theorem by its relationship to the mathematical claim and enforces the classification through AxiomAudit.lean.The classifications are full, library_wrapper, reduced_core, and placeholder; delivery claims count only full and library_wrapper.
- Technical depth: The continuous L^2 Itô integral is constructed as a bounded linear isometry on [0, T].This development reaches the structurally verified object that Nagy’s derivation constructs and leaves.
- Technical depth: The risk-neutral measure is derived rather than assumed through a static Girsanov change of measure, turning BSCallHyp into a theorem.The corresponding Lean result is BSCallHyp.exists_of_physical.
- Technical depth: The binomial-to-Black–Scholes scaling limit is machine-checked end to end using characteristic functions and Lévy continuity, with put-call parity avoiding the uniform-integrability obstruction.The explicit-constant non-asymptotic refinement is deferred to a separate paper.
- Scope and limitations: The project maps its reduced_core frontier precisely, reports contributions to Mathlib and BrownianMotion, and presents certified unification rather than new financial theory.This is described as an honest map of what the formalization establishes and where its limitations lie.
3 Related work and positioning
The library positions itself as shared infrastructure for mathematical finance, extending formalized-finance precedents with broader continuous-time coverage and an audit of theorem faithfulness. Its closest comparisons concern discrete versus continuous Itô theory, derived versus assumed risk-neutral pricing, and focused AMM formalizations.
- Positioning: Formalized finance has mainly appeared at formal-methods venues, while this work presents a verified library directly as shared infrastructure for mathematical finance.The authors frame the library’s value as infrastructure regardless of the novelty type of individual theorems.
- Comparison with prior work: Nagy’s derivation is the closest precedent, with three modules adapted directly while this library constructs the continuous Itô integral and embeds the derivation in a comprehensive development.The adapted modules cover discrete Itô, two-state FTAP, and structural drift.
- Upstream foundations: Mathlib and Degenne’s BrownianMotion provide the upstream foundation, supplying measure theory, conditional expectation, martingales, Gaussian machinery, and pre-Brownian-motion infrastructure.The library reports its contributed-back lemmas separately in Section 7.
4 Architecture: the principle-based design
The library organizes its pricing theory around three reusable principles—linear no-arbitrage pricing, the Garman normal form, and Brownian-motion grounding—rather than instrument-specific derivations. A cross-cutting faithfulness gate enforces honest theorem classification and axiom use at build time.
- Architectural synthesis: Most pricing content follows from accepting the three pricing principles, while the trusted core remains small.The architecture is designed to derive results from reusable principles rather than re-proving each instrument from scratch.
- Pricing principles: A nonnegative linear pricing functional yields put-call parity, the forward price, and call convexity as corollaries of one structure.This replaces instrument-by-instrument proofs with consequences of linearity and non-negativity.
- Pricing principles: The Garman normal form represents Black–Scholes-family prices as A · Φ(d1) − K · DF · Φ(d2), with variants determined by A, DF, and effective volatility.Call, put, digital, power, exchange, dividend, and foreign-rate prices are treated as instances; Margrabe’s exchange-option formula is one such instance.
- Pricing principles: Brownian-motion bridges derive marginal pricing hypotheses from a pre-Brownian motion, connecting flagship prices to the continuous-time object.The bridge starts from the terminal asset being lognormal under Q and establishes the corresponding hypotheses through the BrownianMotion package.
- Faithfulness discipline: The faithfulness gate makes theorem classification and axiom pins build-enforced: dishonest promotion or acquisition of sorryAx causes the build to fail.The gate’s certified cross-domain bridges are presented as concrete products of this discipline.
5 The continuous Itô layer
The library constructs a genuine continuous-time Itô integral rather than assuming or sketching it, extending the adapted isometry from simple processes. It also formalizes surrounding stochastic-calculus results while keeping continuous-time pricing connected through the Section 4 marginal grounding bridge.
- Construction: The library constructs a genuine Itô integral as foundational infrastructure for continuous-time stochastic calculus.The construction is presented as the depth of the library and as a stopping line for the Itô-to-Black–Scholes derivation.
- Construction: The adapted Itô isometry distinguishes random integration from Wiener integration because Brownian-increment cross terms vanish by the weak Markov property.This isometry is established for simple adapted processes before extension.
- Construction: A π–λ density argument and norm-preserving extension carry the isometry from simple adapted processes to the continuous integral.The supplied passage identifies these as the mechanisms completing the construction, with the resulting integral formalized in ItoIntegralBrownian.lean.
- Stochastic-calculus core: The stochastic-calculus core also formalizes Brownian quadratic variation, the integral as a continuous L2 martingale, and Itô formulas for bounded-derivative and unrestricted C3 functions.The unrestricted case uses localization at exit times and yields a compensated residual that is a continuous local martingale.
- Pricing connection: Continuous-time pricing reaches the constructed integral through the Section 4 marginal grounding bridge, not by integrating against itoIntegralCLM_T.The continuous integral is described as foundational infrastructure, while the companion paper develops the full construction and pathwise theory.
6 Deriving the risk-neutral measure
The library derives, rather than assumes, equivalent martingale measures through static and dynamic Girsanov constructions. These measures ground Black–Scholes and Margrabe pricing results and support no-arbitrage consequences across several market settings.
- Static derivation: The library derives the pricing measure via an Esscher-density Girsanov change, producing the terminal lognormal asset law required by pricing formulas.This replaces the usual assumption of an equivalent martingale measure with a construction from the physical Gaussian-driver law.
- Dynamic derivation: Girsanov’s theorem is formalized dynamically for constant, simple, continuous-adapted, and bounded-predictable drifts.Under the corresponding exponential-martingale measure, the drift-adjusted Brownian motion is a Q-Brownian motion.
- No-arbitrage consequence: An equivalent martingale measure on a continuous market precludes arbitrage against simple predictable strategies, with discounted geometric Brownian motion as the worked instance.This provides the forward, model-agnostic half of the first fundamental theorem of asset pricing.
- Pricing consequences: The derived measure turns the Black–Scholes call formula into a statement about the physical model and grounds Margrabe’s exchange-option formula through the same change of numéraire.The library reuses the measure change rather than introducing a fresh derivation for Margrabe’s formula.
- Market-specific constructions: Fundamental-theorem results construct equivalent martingale measures using Hahn–Banach separation in finite-state models and smooth convex-potential minimisation in general one-period models.The latter covers both one-asset and d-asset settings.
7 Evaluation and contributed lemmas
The evaluation covers 330 theorems, of which 316 are delivery-claim-ready, with reduced cores concentrated at the continuous-time frontier. A reproducible, axiom-audited build validates the sorry-free library and documents upstream API contributions and newly developed integral lemmas.
- Faithfulness evaluation: 330 benchmark theorems are tracked by the coverage report and classified into faithfulness tiers.The classification is presented in Table 2.
- Faithfulness evaluation: 316 of 330 theorems are delivery-claim-ready, while reduced-core items cluster in continuous-time and discrete-process benchmarks.The mathematical-finance benchmark is almost entirely full, whereas partial cores occur at the genuinely hard continuous-time frontier.
- Reproducibility and audit: The repository build compiles the whole library and its AxiomAudit gate, machine-checking that audited results are sorry-free and use only Lean’s three standard axioms.The three axioms are propext, Classical.choice, and Quot.sound.
- Reproducibility and audit: Lean v4.31.0, Mathlib fabf563a, BrownianMotion bdf5ea0c, and a pinned Docker image make the approximately 52,300-line library reproducible.The versions are pinned in lean-toolchain and lake-manifest.json, and the Docker image reproduces the build.
- Contributed lemmas: The work contributed a stochastic time-interval API upstream and developed Gaussian-tail and completing-the-square integral lemmas absent from Mathlib.The integral lemmas supported the pricing proofs.
8 Conclusion
The library’s main contributions are deep formal constructions and a faithfulness audit that makes mathematical-finance claims logically checkable. Its machine-checked classical theory unifies known results rather than producing new financial theory, providing a methodological and infrastructural verified foundation.
- Core contributions: The library’s two substantive contributions are a constructed continuous Itô integral, a derived risk-neutral measure, and an audit of each claim’s logical status.The audit makes the status of every claim checkable.
- Scope of contribution: Machine-checking classical financial mathematics yields certified unification of known results, not new financial theory.The contribution is therefore methodological and infrastructural: a verified foundation for mathematical finance.
- Faithfulness audit: Tier classification and an axiom gate make the library’s faithfulness checkable.These mechanisms expose the logical status and axioms used by its proofs.
- Future development: Companion work develops the continuous Itô integral, the static-Girsanov derivation of the risk-neutral measure, and an explicit non-asymptotic binomial-to-Black–Scholes convergence bound.The conclusion identifies these results as continuing companion-paper developments.