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ô 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.
Alex: Welcome to another episode of ResearchPod.
Sam: Today we're looking at a project that tries to bring computer-checked proof to the world of financial mathematics. The central question it addresses is whether we can actually trust the complex math behind our financial models — by creating what the authors call a "faithfulness audit" that maps exactly what assumptions each proof relies on.
Alex: So it's like a nutrition label for financial proofs? You can see exactly what ingredients — or assumptions — went into the result?
Sam: That's a good way to put it. In mathematics, a proof is only as strong as its foundation. If a researcher uses a shortcut or an unstated assumption, the entire model might be built on shaky ground. This project forces every proof to explicitly list its dependencies, so those silent, hidden assumptions can't quietly sneak in.
Alex: Why is that particularly difficult in finance?
Sam: Financial math often relies on what are called continuous-time models — math that describes things changing every single instant, not just from day to day. To build that kind of model, you need to handle some genuinely tricky concepts. One of the trickiest is something called the Itô integral. Think of it like trying to measure the exact path of a leaf blowing in the wind. The leaf doesn't move in neat, predictable steps — it's constantly being nudged by random gusts. The Itô integral is the mathematical tool that lets you calculate things about processes that are that noisy and unpredictable.
Alex: And most previous work just assumed those pieces were solid, rather than building them from scratch?
Sam: Precisely. Earlier work either took those foundations for granted or only sketched them out informally. This library actually constructs the Itô integral from the ground up — in a way that guarantees the math is perfectly consistent throughout, rather than just assuming it works.
Alex: You mentioned a "faithfulness audit." How does that actually work in practice?
Sam: Every proven result in the library gets a label based on how honestly it represents what it's claiming. Some results are fully verified, with every single logical step confirmed. Some are re-exports of existing verified work. And some fall into a category the authors call "reduced core," meaning they still rely on extra hypotheses that haven't been fully proven yet. The key is that a build-enforced gate checks these labels automatically. If a proof tries to sneak in an unproven assumption without declaring it, the system refuses to compile — it simply won't run.
Alex: So the computer acts like a strict editor that rejects the work if it doesn't show its full, honest reasoning?
Sam: Exactly. The goal is for results to be what the authors call "sorry-free" — meaning there are no placeholders where a researcher just wrote "let's assume this part works." Every gap has to be declared openly. It forces total transparency about where the proof is still relying on unverified ground.
Alex: That sounds like a significant undertaking. How much did they actually manage to verify?
Sam: They verified 251 theorems across eleven different areas of finance — covering everything from basic portfolio theory to complex derivative pricing models, including the well-known Black-Scholes formula. The authors describe it as the most comprehensive machine-checked development in this field to date.
Alex: You mentioned this doesn't produce new financial theory. Does that mean the project is limited in what it can offer?
Sam: It's worth being clear about that distinction. The authors are candid: this is foundational work, not generative work. It doesn't tell us how to make better predictions about markets. What it does instead is provide a certified, unified language for existing classical finance. It demonstrates that different models — developed independently, often using different notation and methods — are actually describing the same underlying mathematical structures.
Alex: So it's like taking a dozen different textbooks that all use different symbols, and proving they're all talking about the same thing?
Sam: That's a very apt way to put it. By unifying these definitions, the library becomes shared infrastructure. It's a standard reference point for quantitative finance, ensuring that when researchers use terms like "risk" or "variance," they're working from verified, consistent definitions — not subtly different ones that could quietly lead to different conclusions.
Alex: What about the risk-neutral measure? That seems like a central piece of how financial models price things.
Sam: It is. In most models, researchers simply assume this measure exists because it makes the math tractable. Think of it as a kind of convenient fiction — you reframe the world so that all assets appear to grow at the same rate, which simplifies the pricing formulas enormously. This library doesn't just assume it exists. It derives it, using what the authors call a static Girsanov change. That means the measure is shown to follow logically from the physical model of how the asset actually behaves — rather than being introduced as a convenient starting point.
Alex: So they're removing the shortcuts that researchers usually take to get to the final price?
Sam: Right. By deriving the measure rather than assuming it, the final pricing formula becomes a statement about the actual, physical model — not just a result that falls out of an artificial mathematical environment. The entire chain of logic becomes more robust.
Alex: It feels like this level of strictness could change how researchers document their work. But is there a cost to it?
Sam: The main trade-off is the sheer effort involved. Formalizing mathematics is slow and demanding. You have to be precise about every single logical step — there's no room for hand-waving. It's not a practical approach for every piece of research. But for critical financial models, where errors can have real consequences, this kind of rigor represents a meaningful improvement over informal verification.
Alex: Where does the work go from here?
Sam: The authors note that this is a beginning, not an endpoint. The "reduced core" theorems — the ones still relying on some unproven hypotheses — are the natural next target. Future work could extend the library into pathwise calculus and stochastic differential equations, gradually building toward a truly universal, verified standard library for quantitative finance.
Alex: So even if it doesn't uncover new market insights today, it builds the infrastructure that makes future discoveries more reliable.
Sam: That's the core contribution. It's about creating a foundation of trust. By making the mathematics checkable — step by step, assumption by assumption — we can be more confident that the models we rely on are as rigorous as the markets they attempt to describe. Thanks for listening to ResearchPod.