formal-mathfin

A library of mathematical finance in Lean 4, built on Mathlib and BrownianMotion. It covers stochastic calculus (the Itô integral, Itô's formula, Girsanov's theorem, martingale representation, stochastic differential equations), no-arbitrage theory, derivative pricing, fixed income, portfolio theory, risk measures and actuarial mathematics.

The corpus records 535 results from the literature in benchmarks/, each with a Lean statement and proof. Of these, 504 are proved in full, 18 restate a lemma from Mathlib or BrownianMotion, and 13 are reduced cores that prove less than the result they are named after. Each entry records its status and what it leaves out. The library contains no sorry, and a build-time audit checks that every library theorem the benchmark's proofs cite depends only on the axioms propext, Classical.choice and Quot.sound.

Here, for example, is the convergence of the Cox–Ross–Rubinstein call price to the Black–Scholes price, from CRRClosedForm.lean:

theorem binomialPrice_call_tendsto_bs_closed {r σ T S₀ K : ℝ}
    (hσ : 0 < σ) (hT : 0 < T) (hS₀ : 0 < S₀) (hK : 0 < K)
    (hna : ∀ n, 0 < n → BinomialNoArb (crrUp σ T n) (crrDown σ T n) (crrPerStepRate r T n)) :
    Tendsto (fun n : ℕ ↦ binomialPrice (crrUp σ T n) (crrDown σ T n) (crrPerStepRate r T n)
        (fun x ↦ max (x - K) 0) n S₀) atTop
      (𝓝 (S₀ * Phi (bsd1 S₀ K r σ T)
          - K * Real.exp (-(r * T)) * Phi (bsd2 S₀ K r σ T)))

The hypothesis hna, that the -step tree is free of arbitrage for every , holds whenever (binomialNoArb_crr).

Main results

• Itô's formula. For every function , with no growth condition, is a continuous local martingale (ito_formula_unrestricted). When the partial derivatives of are bounded, its value at time is the Itô integral (ito_formula_td_L2_bddDeriv). For an Itô process with bounded adapted continuous coefficients, and with and bounded, $`f(X_T) - f(x_0) = \int_0^T f'(X_s)\sigma_s,dB_s

  • \int_0^T \big(f'(X_s) b_s + \tfrac12 f''(X_s)\sigma_s^2\big),ds$ almost surely ([ito_formula_adapted`](MathFin/Foundations/ItoFormulaAdapted.lean)).

• Girsanov's theorem. For bounded predictable , let . On , under , the process starts at and has independent increments, so its finite-dimensional laws are those of a Brownian motion (Btheta_isQBrownianMotion_predictable_of_bdd, stated for an adapted modification of the process, which has the same finite-dimensional laws).

• Martingale representation. Every square-integrable, -measurable random variable can be written for a unique . In trading terms, each such claim is replicated from initial wealth by a unique strategy (exists_replicating_strategy).

• Stochastic differential equations. If and are Lipschitz with constants and , the Picard map of has a unique fixed point in the space of predictable processes on whenever (picardMap_exists_unique_fixedPoint).

• Fundamental theorem of asset pricing. A market with one risky asset, finitely many periods and a finite probability space of full support has no arbitrage if and only if it has an equivalent martingale measure (ftap_discrete). The one-period theorem holds on any probability space with finitely many assets (ftap_one_period_vector).

• Coherent risk measures. On a finite state space, a coherent risk measure satisfies , where is the set of probability vectors that give every acceptable position a nonnegative price (coherentRisk_isLUB). This theorem and the finite fundamental theorem are both derived from the cone-separation lemmas in ConvexDuality.lean.

• The Black–Scholes PDE from Feynman–Kac. The call price is written as a heat-kernel integral, and the Black–Scholes PDE follows from the heat equation for the kernel, without differentiating the closed-form price (bsV_satisfies_bs_pde_via_feynmanKac).

• Jump-diffusions. Let be adapted and start at , with each increment independent of the past and distributed as , where , , and the jumps are i.i.d. with law , all independent. If and , the discounted price is a martingale exactly when (JumpDiffusionProcess.martingale_iff). At that drift, with Gaussian jumps and , the conditional expectation of the discounted call payoff at every date before maturity is Merton's 1976 series (condExp_call_eq_mertonCallPrice).

• The American put. In the Black–Scholes model with interest rate and dividend yield , the early-exercise boundary of the American put is strictly convex in the time to expiry, and is convex (PhysicalBoundaryConvexity.lean, described in docs/american-put-boundary.md).

• Raw SVI. A fixed finite Boolean combination of signs of polynomials in the five parameters holds exactly when , , , the SVI total variance is positive at every log-strike, and the Black–Scholes call with the SVI volatility substituted strike by strike is convex in the strike. For that convexity is Durrleman's condition (extendedCertificateFormula_iff_bsSmile_convex, bsSmile_convex_iff). With one more sign, , the formula holds exactly when, in addition, that call is nonincreasing in the strike, lies between and , and tends to at strike and to at large strikes (butterflyFreeFormula_iff_isNormalizedCallPrice).

Contents

Area	Topics
Probability	conditional expectation, martingales and stopping times, Brownian motion, Poisson processes, Markov chains
Stochastic calculus	Itô integral and isometry, quadratic variation, Itô's formula, Girsanov's theorem, martingale representation, SDEs, Feynman–Kac, compensated Poisson integral
No-arbitrage	fundamental theorems, equivalent martingale measures, change of numéraire, market completeness, superreplication
Option pricing	Black–Scholes prices and Greeks, the Black–Scholes PDE, implied volatility, dividends, FX (Garman–Kohlhagen), Bachelier, Black-76, jump-diffusions (Merton's formula and Greeks, Esscher pricing, incompleteness at one date), Breeden–Litzenberger, a polynomial-sign certificate for strike-convexity of raw SVI
Exotic options	digital, exchange (Margrabe), chooser, barrier, lookback, geometric Asian, power and quanto options; spreads; variance swaps
Lattice models	binomial replication, American and Bermudan options via the Snell envelope, Cox–Ross–Rubinstein convergence, André's reflection principle
Fixed income and credit	bonds, duration and convexity, immunization, yield curves, forward rates, FRAs, swaps and swaptions, the forward measure, Vasicek, hazard rates, CDS, first-to-default, KMV–Merton
Portfolio theory	Markowitz, CAPM, two-fund separation, the tangency portfolio, risk parity, Black–Litterman; Sharpe, Sortino, Treynor and information ratios; the Kelly criterion
Risk measures	the quantile function; value-at-risk and expected shortfall for every law: Rockafellar–Uryasev, coherence of ES, its dual representation, VaR superadditivity, elicitability (VaR yes, ES no), expectiles; coherent and spectral risk measures, expected utility, concentration indices
Dependence and extremes	copulas and Sklar's theorem (continuous margins), Fréchet–Hoeffding bounds, Hoeffding's covariance identity, Marshall–Olkin common shocks; GEV and GPD domains of attraction, maxima of Poisson-many losses
Credit portfolios	Bernoulli mixtures, the one-factor Gaussian threshold model, and the Basel IRB formula as the limit of portfolio VaR
Market microstructure	Avellaneda–Stoikov market making, the Glosten–Milgrom spread
Other	a contract language that separates payoffs from pricing models; survival models, mortality and annuities; compound Poisson losses; constant-product AMMs

Limitations

• Thirteen of the 535 results are reduced cores. Twelve assume a structure whose fields include the textbook conclusion, so the conclusion is not derived: the reflection principle, nowhere differentiability and the law of the iterated logarithm for Brownian motion, Novikov's condition, the general form of Girsanov's theorem, Lévy's characterization, the two-dimensional Itô formula, and five theorems on Markov chains. The thirteenth proves a special case: the first interarrival time of a Poisson process is exponential.
• Girsanov's theorem is proved only for bounded predictable , and, as for itself, only at the level of finite-dimensional laws: neither path continuity of the new process nor independence of its increments from the past is stated.
• Of the second fundamental theorem, only the direction from completeness to uniqueness is proved: for a price with almost everywhere, a probability measure with square-integrable density with respect to , under which is a martingale, agrees with on .
• Martingale representation proves that a hedge exists and is unique, but does not identify it; that needs the Clark–Ocone formula (#182, open).
• The SVI certificate's formula is defined structurally, not written out as a list of inequalities. Butterfly-freeness is proved as a list of properties of the call price as a function of the strike; the risk-neutral law is not constructed from them. At convexity of the call is not tied to Durrleman's condition.
• Itô's formula for an Itô process is proved at a fixed time, for bounded adapted continuous coefficients and with bounded and . It does not yet cover or , or coefficients of an SDE solution.
• The jump-diffusion results on a process assume the properties listed above (JumpDiffusionProcess). A process with them is constructed only without jumps, as Brownian motion with drift. A change of measure on the process that alters the jump rate or the jump law is not covered.
• Existence for SDEs with Lipschitz coefficients is proved only on horizons with .
• The binomial limit is proved for call prices and for the law of the terminal log-return. Convergence of the price process (Donsker's invariance principle) is not formalized.
• The multi-period fundamental theorem and the representation of coherent risk measures are proved on finite probability spaces only.

Building

With elan installed:

git clone https://github.com/formal-applied-math/formal-mathfin.git
cd formal-mathfin
lake exe cache get   # prebuilt Mathlib
lake build

lean-toolchain pins the Lean version and lake-manifest.json pins Mathlib and BrownianMotion. BrownianMotion and the library itself are compiled from source. CONTRIBUTING.md describes a prebuilt Docker image and a faster edit-and-check loop for contributors.

Verification

A successful lake build checks every proof in the library. The benchmark entries are not Lake targets and are checked separately (see Benchmark below). In this repository, sorry appears only in the two theorems of Challenge.lean, which are left unproved on purpose (see Comparator below).

• Axioms. MathFin/AxiomAudit.lean and the generated MathFin/AxiomAuditGen.lean run #print axioms on a curated list of headline results and on every library constant that a benchmark entry's proof cites, and compare the output with #guard_msgs. A sorry or an extra axiom anywhere in the proof of one of them fails the build. Citations are found by where a name is declared, so a name cited under open, by dot notation, or from a namespace other than MathFin is covered. The Mathlib and BrownianMotion theorems that library_wrapper entries re-export are pinned too: BrownianMotion has sorrys of its own, and none of those theorems depends on one.

• Comparator. Challenge.lean states the coherent-risk representation theorem, with a witness that its hypothesis is satisfiable, using only Mathlib; Solution.lean proves both from the library. Comparator, configured by comparator.json, checks that the two files state the same theorems and that the proofs use only the three standard axioms. It accepted both at commit 06f88ca and is not run in CI; see docs/palomar.md.

• Benchmark. Each entry in benchmarks/ records a result's Lean statement, its status and its scope. The ledger runner, tools/verify/ledger.py, checks each entry's snippet against the library, and verification_ledger.json stores a hash of the inputs it was checked under; CI fails if any entry's inputs have changed since. The entries are published as a Hugging Face dataset.

• Kernel replay. A workflow replays every declaration through leanchecker, but the full Mathlib environment it loads does not fit on a 16 GB hosted runner, and the replay has not completed.

• Provenance. formalization.yaml describes how the library was written, including AI assistance and the entries drafted by an automated pipeline. The American put port records its own provenance in docs/american-put-boundary.md.

Documentation

• docs/coverage.md: a dated log of status changes and corrections, with verification evidence.
• docs/blueprint.md: a dependency graph from Brownian motion to Black–Scholes, generated from the Lean source.
• docs/mathematical-architecture.md: the principles the library is organized around, and the theorems that connect them.
• MathFin/Examples.lean: five representative proofs.
• docs/open-problems.md: a survey of open problems in mathematical finance.
• docs/roadmap.md and the issue tracker: planned work.
• docs/README.md: an index of the remaining documents.

Contributing

Contributions are welcome. CONTRIBUTING.md explains how to add a theorem, and docs/onboarding.md walks through a first contribution. Issues labelled good first issue are the usual starting point.

Citation

@article{coelho2026mathfin,
  title   = {A Formally Verified Library of Mathematical Finance in {Lean} 4},
  author  = {Coelho, Raphael},
  journal = {arXiv preprint arXiv:2606.01356},
  year    = {2026},
  doi     = {10.48550/arXiv.2606.01356}
}

To cite the software itself, use the Zenodo DOI 10.5281/zenodo.20477781, which resolves to the latest release. Both are in CITATION.cff.

Acknowledgements

The library depends on Mathlib and on BrownianMotion, the formalization of Brownian motion and stochastic integration led by Rémy Degenne. Much of the benchmark follows Yuri F. Saporito's Stochastic Processes. The contract language takes its design ideas, but no code, from Paul Bilokon's The Contract Is Not the Model (2026), and the survival models draw on Yosuke Ito's Archive of Formal Proofs entry on actuarial mathematics (docs/sources.md). The American put results are ported from Robert Martin's AmericanPutConvexity, and the SVI polynomial-sign certificate from his ButterflyFreeSVI.

License

Apache 2.0. See LICENSE.