pith. sign in

arxiv: 2606.01356 · v2 · pith:YXJNNJ3Znew · submitted 2026-05-31 · 💱 q-fin.MF · q-fin.CP

A Formally Verified Library of Mathematical Finance in Lean 4

Raphael Coelho This is my paper

Pith reviewed 2026-06-30 11:14 UTC · model grok-4.3

classification 💱 q-fin.MF q-fin.CP
keywords formal verificationmathematical financeLean 4Itô integralrisk-neutral measurestochastic calculusproof assistantfaithfulness audit
0
0 comments X

The pith

A Lean 4 library constructs the L² Itô integral as a bounded linear isometry and derives the risk-neutral pricing measure.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper builds a library in the Lean 4 proof assistant that contains more than two hundred theorems without placeholders across eleven areas of mathematical finance. It starts from measure-theoretic stochastic calculus and extends to derivative pricing, portfolio theory, and fixed-income models. The development constructs the L² Itô integral as an isometry and derives the risk-neutral pricing measure instead of assuming it. It also classifies every theorem by the exact relation between its formal statement and the mathematics it intends to capture, while enforcing a build-time record of the axioms actually used. The result is a reusable, machine-checked foundation that unifies existing results rather than introducing new financial claims.

Core claim

The library reaches continuous-time theory far enough to construct the L² Itô integral as a bounded linear isometry and to derive the risk-neutral pricing measure from first principles; every result carries an explicit classification of how its Lean statement relates to the intended classical claim, and a build gate records the precise axioms used in each proof.

What carries the argument

The faithfulness classification of each Lean statement combined with a build-enforced gate that records the axioms actually used in each proof.

If this is right

  • Readers can inspect precisely which results hold unconditionally and which depend on added hypotheses.
  • The verified foundations become reusable building blocks for further formal work in continuous-time finance.
  • Known pricing and risk results are shown to follow from a single formal base without separate assumptions.
  • The same classification and gate mechanism can be applied to other developments in stochastic calculus.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The audit system could be reused to check formalizations of related continuous-time models in physics or engineering.
  • Once the library exists, one could test whether adding a new pricing formula preserves the existing risk-neutral derivation.
  • The approach suggests a route to machine-checked consistency checks across different textbooks that present the same formulas under slightly different axioms.

Load-bearing premise

The mapping from each Lean theorem statement to its intended classical mathematical claim has been performed correctly.

What would settle it

Discovery of a theorem in the library whose Lean statement is shown to be strictly stronger or weaker than the informal claim it is classified as matching, or an axiom used in a proof that the gate did not record.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript presents a Lean 4 library for mathematical finance built on Mathlib and the BrownianMotion package. It contains more than 200 sorry-free theorems spanning eleven areas from measure-theoretic stochastic calculus through derivative pricing, risk, portfolio theory, and fixed-income. The library constructs the L² Itô integral as a bounded linear isometry and derives the risk-neutral pricing measure rather than assuming it; every result is classified by faithfulness to the intended classical statement and a build-enforced gate records the axioms actually used.

Significance. The work supplies a reusable, machine-checked foundation for continuous-time mathematical finance. The mechanical verification of the L² Itô isometry and the derivation of the risk-neutral measure, together with the explicit faithfulness classification and axiom audit, constitute a methodological contribution that enables certified unification of known results. These features are load-bearing strengths for any subsequent formal development that relies on the library.

minor comments (2)
  1. A summary table listing the eleven areas together with the approximate number of theorems per area would improve navigability for readers.
  2. The abstract states that the contribution is 'methodological and infrastructural'; a brief sentence in the introduction clarifying how the faithfulness classification is implemented (e.g., which Lean attributes or custom commands enforce the gate) would help readers locate the mechanism.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for the recommendation to accept. The report accurately captures the scope of the library, the construction of the L² Itô integral as a bounded linear isometry, the derivation of the risk-neutral measure, and the built-in faithfulness and axiom-audit mechanisms.

Circularity Check

0 steps flagged

No significant circularity; formalization derives results from base axioms

full rationale

The paper is a machine-checked formalization in Lean 4 that constructs the L² Itô integral and derives the risk-neutral measure from the axioms of Mathlib and the BrownianMotion package. All theorems are sorry-free and audited for faithfulness via an explicit classification and build-enforced axiom gate. No financial quantities are fitted to data, no predictions reduce to prior fitted parameters, and no load-bearing self-citation or ansatz is invoked to justify the central claims. The derivation chain is therefore self-contained within the proof assistant and does not reduce to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The library depends on the axioms and definitions supplied by Mathlib and the BrownianMotion package; no new free parameters, ad-hoc axioms, or invented entities are introduced for the financial results themselves.

axioms (2)
  • standard math Standard axioms and definitions of Mathlib (classical logic, measure theory, topology, etc.)
    All proofs are built on top of Mathlib; the paper does not add new mathematical axioms.
  • domain assumption Definitions and theorems from the BrownianMotion package
    The library is explicitly built on this package for stochastic processes.

pith-pipeline@v0.9.1-grok · 5759 in / 1346 out tokens · 32285 ms · 2026-06-30T11:14:09.908666+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. The Fundamental Theorem of Asset Pricing, Formalized in Lean 4

    q-fin.MF 2026-06 accept novelty 9.0 full

    First machine-checked formalization of the FTAP in Lean 4 across three settings, with explicit EMM construction via minimization of E[log(1+e<θ,Y>)] in the d-asset case.

  2. A Machine-Checked It\^o Calculus for Brownian Motion

    q-fin.MF 2026-06 accept novelty 8.0 full

    Lean 4 formalization of the Itô integral as Hilbert-space isometry from simple processes, Itô's formula for C3 functions with explicit L2 bounds, and extension to continuous local martingale.

Reference graph

Works this paper leans on

12 extracted references · 3 canonical work pages · cited by 2 Pith papers · 1 internal anchor

  1. [1]

    Black and M

    F. Black and M. Scholes. The pricing of options and corporate liabilities.Journal of Political Economy, 81(3):637–654, 1973

    1973

  2. [2]

    Degenne et al.brownian-motion: a Lean 4 development of Brownian motion

    R. Degenne et al.brownian-motion: a Lean 4 development of Brownian motion. https: //github.com/RemyDegenne/brownian-motion, 2024–2026

    2024

  3. [3]

    J. C. Cox, S. A. Ross, and M. Rubinstein. Option pricing: a simplified approach.Journal of Financial Economics, 7(3):229–263, 1979

    1979

  4. [4]

    Echenim and N

    M. Echenim and N. Peltier. The binomial pricing model in finance: a formaliza- tion in Isabelle. InAutomated Deduction – CADE-26, LNCS 10395. Springer, 2017. doi:10.1007/978-3-319-63046-5_33. Extended version:Journal of Automated Reasoning, 63, 2019, doi:10.1007/s10817-019-09528-w

    work page doi:10.1007/978-3-319-63046-5_33 2017

  5. [5]

    J. M. Harrison and D. M. Kreps. Martingales and arbitrage in multiperiod securities markets.Journal of Economic Theory, 20(3):381–408, 1979

    1979

  6. [6]

    R. Coelho. A machine-checked Itô calculus for Brownian motion. arXiv:2606.15089, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  7. [7]

    de Moura and S

    L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE-28, LNCS 12699, pages 625–635. Springer, 2021

    2021

  8. [8]

    Margrabe

    W. Margrabe. The value of an option to exchange one asset for another.Journal of Finance, 33(1):177–186, 1978

    1978

  9. [9]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. InProc. 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs (CPP 2020), pages 367–381. ACM, 2020

    2020

  10. [10]

    T. Nagy. From Itô to Black–Scholes: a machine-verified derivation in Lean 4. SSRN preprint 6336503, 2026.https://papers.ssrn.com/sol3/papers.cfm?abstract_id=6336503

    2026

  11. [11]

    Pusceddu and M

    D. Pusceddu and M. Bartoletti. Formalizing automated market makers in the Lean 4 theorem prover. In5th Int. Workshop on Formal Methods for Blockchains (FMBC 2024), OASIcs

    2024

  12. [12]

    doi:10.4230/OASIcs.FMBC.2024.5, arXiv:2402.06064

    Schloss Dagstuhl, 2024. doi:10.4230/OASIcs.FMBC.2024.5, arXiv:2402.06064. 7

    work page doi:10.4230/oasics.fmbc.2024.5 2024