A Formally Verified Library of Mathematical Finance in Lean 4

In quantitative finance, the distance between a theoretical model and a production implementation is often bridged by "hand-waving." This refers to the implicit assumption that certain mathematical properties, like the existence of a risk-neutral measure, simply hold. Researchers have recently attempted to close this gap. They have created massive digital libraries that use advanced computer logic to prove that complex financial formulas are mathematically perfect.

Until now, formal verification in finance has been narrow and fragmented. Previous work focused on isolated models, like the discrete Cox–Ross–Rubinstein model. Other work provided single-path derivations that skipped the heavy lifting of stochastic calculus (the study of continuous-time random processes). There was no unified framework to verify the entire stack from measure-theoretic foundations up to applied portfolio theory. This paper introduces a library in the Lean 4 proof assistant to provide that missing infrastructure.

The Problem

The current state of formalized finance suffers from two main issues: shallow depth and lack of transparency. Existing formalizations often treat the continuous Itô integral as a structural given. This integral is the mathematical engine behind stochastic calculus. Instead of actually constructing it, they simply assume it exists. This means the "proof" might be valid, but it rests on an unverified foundation.

Furthermore, there is a significant "faithfulness gap" in formal methods. When a researcher claims to have proved a financial theorem, they often omit details. They may rely on additional, unstated hypotheses or heavily axiomatized sub-steps. In a production environment, this ambiguity is dangerous. It creates a false sense of security regarding how much of the model is truly "certified" versus how much is merely being assumed.

How It Works

The authors implement a broad, principle-based architecture in Lean 4. It is designed to minimize the trusted core while maximizing coverage. Rather than proving every financial instrument from scratch, the library derives results from four key pillars:

1. Linear No-Arbitrage Pricing Functionals: Pricing is modeled as a non-negative linear functional on payoffs. By establishing this single structure, the authors can derive put-call parity and the convexity of calls as mere corollaries. This reduces the total surface area for potential errors.
2. The Garman Normal Form: The library recognizes that most Black–Scholes variants share a common mathematical structure ($A \cdot \Phi(d_1) - K \cdot DF \cdot \Phi(d_2)$). This allows diverse options—digital, power, and exchange—to be treated as specific instances of a single template.
3. Brownian-Motion Grounding: To connect high-level pricing models to low-level stochastic processes, the authors use "bridges." These show that pricing hypotheses follow logically from the underlying Brownian motion infrastructure.
4. The Faithfulness Gate: This is the library's most significant methodological contribution. Every theorem is classified into one of four tiers: full (the statement is the claim), library_wrapper (a thin re-export), reduced_core (holds under extra hypotheses), or placeholder. To prevent "logic drift," the authors use a build-enforced gate called AxiomAudit.lean. This script pins the exact axioms used in every load-bearing theorem. If a developer accidentally introduces an unverified assumption or a "sorry" (a placeholder for unproven code), the entire library fails to compile.

Numbers

The authors report a massive scale of formalization. They have produced 251 "sorry-free" theorems across eleven distinct areas of finance. This means every proof is complete and contains no unverified placeholders. This represents approximately 24,800 lines of Lean 4 code.

The paper provides a breakdown of the faithfulness tiers to show reliability. Of the 251 theorems, 204 are classified as full and 19 as library_wrapper. This means 223 of the 251 theorems meet the highest standards of delivery-claim readiness. The reduced_core theorems—those requiring extra hypotheses—account for 28 results. These are primarily clustered around the difficult continuous-time frontiers.

What's Missing

While the library is impressive in breadth, it has clear boundaries. First, the authors admit this is a methodological achievement rather than a discovery of new financial theory. The library certifies that existing classical mathematics is consistent. It does not generate new insights into market behavior.

Second, while the library constructs the continuous $L^2$ Itô integral and derives the risk-neutral measure, the full technical details are deferred. These details are reserved for companion papers currently in preparation. For a practitioner looking to inspect the exact low-level mechanics of the Girsanov change-of-measure implementation, the current version acts as a high-level verified interface. Finally, the library does not yet address pathwise Itô calculus or stochastic differential equations (SDEs). These remain on the "open frontier" of the project.

Should You Prototype This

If you are building mission-critical quantitative models, the faithfulness-audit methodology is worth prototyping. The cost of a mathematical error can be catastrophic. Even if you do not adopt the entire Lean 4 library, the concept of pinning axioms to prevent "logic drift" is a powerful pattern. It is useful for any high-assurance software system.

However, do not look for a ready-to-use library to plug into a production trading engine next week. The library is a foundational infrastructure project, not a turnkey solver. You can explore the existing codebase at the reported artifact link: https://github.com/raphaelrrcoelho/formal-mathfin. Use it to audit your own internal mathematical definitions. Do not expect it to replace your existing modeling stack until the companion papers are released.