MathFin | Reservoir

Mathematical finance, formally verified

A Lean 4 library building toward a formal theory of mathematical finance — every result machine-checked against Mathlib and Degenne's BrownianMotion, with an exact statement of what is proved and what is assumed, and the deep connections between the field's pillars made load-bearing rather than decorative.

319 theorems · 304 delivery-ready · 0 sorries · axioms-clean · lake build is the proof.

What we're building

Formalized finance is usually a scattering of isolated results. The ambition here is a theory: prove the Black–Scholes world, the Itô tower, the Fundamental Theorem of Asset Pricing, and the risk-measure layer — then wire them together around the field's actual organizing principles, so that the architecture is the artifact, not just the catalogue. "Top-notch" here is not more theorems — it is the theorems organized around the field's spine, with the deep cross-connections proved.

Two commitments make that trustworthy:

The build is the proof. A clean lake build re-elaborates every theorem against pinned Lean + Mathlib. There is no sorry and no project-local axiom anywhere; every full result depends only on the three standard axioms propext, Classical.choice, Quot.sound, #print axioms-pinned as a CI invariant in MathFin/AxiomAudit.lean.
Honest scope, enforced — never overclaimed. Every entry declares a faithfulness status (full / library_wrapper / reduced_core); an input-hash verification ledger records exactly what each was checked under; and a multi-agent values review runs on a CI cadence. The README does not claim a result the kernel has not accepted.

The architecture — the field's spine

Mathematical finance is a few deep principles whose consequences are the models. The library has the four pillars; the active program is to make the connective tissue between them load-bearing.

Pillar	The principle	In the library
I — No-arbitrage as convex duality	the separating hyperplane is the equivalent martingale measure	the FTAP tower · `ConvexDuality` · state prices
II — Stochastic calculus	every model is `dX = b dt + σ dB`; Itô makes functionals computable	the Itô tower: from-scratch L² integral, Itô's formula, quadratic variation
III — Probabilistic ⟷ analytic duality	the price is both a risk-neutral expectation and a PDE solution	the BS-PDE keystone (Feynman–Kac and Itô routes)
IV — Intensity & exponential families	closed forms and the "exp of an integrated intensity"	Gaussian closed forms · the exponential-discount root · credit/mortality unification

The bridges are where the depth lives — each makes two pillars one theorem:

Bridge	Connects	Status
Convex duality	I ↔ IV (pricing ↔ risk)	✅ WIRED — the FTAP and the coherent-risk representation are proved to be the same Hahn–Banach theorem
Feynman–Kac	II ↔ III	✅ WIRED — the Black–Scholes PDE from the risk-neutral expectation
Donsker / CLT	discrete ↔ continuous	✅ WIRED — CRR binomial → Black–Scholes
Girsanov	I ↔ II	◐ wired — bounded case closed — the EMM is an explicit change of measure, and the distributional Girsanov is now fully closed for bounded predictable θ (the honest Itô-`L²` domain): `B^θ = B + ∫θ ds` is a `Q`-Brownian motion (Gaussian and independent increments) under `Q = withDensity(exp(−∫θ dB − ½∫θ² ds))`; only the general `L²`/progressive-θ (Novikov, unbounded) case stays open
Numéraire	IV ↔ I	✅ WIRED — the price-invariance seam `N₀·𝔼^{Qᴺ}[X/N_T] = B₀·𝔼^Q[X/B_T]` (`changeOfNumeraire`), with BS-stock / Margrabe-`S²` / Kelly-EMM instances

→ The full spine, seam by seam: docs/mathematical-architecture.md.

Landmark results

Result	Statement	Lean
Pricing = risk, one theorem	the FTAP separating functional and the coherent-risk representation are the same finite-dimensional Hahn–Banach separation	`exists_pos_separating_of_cone_disjoint_simplex` · `coherentRisk_isLUB`
BS PDE from Feynman–Kac	the Black–Scholes PDE derived from the risk-neutral expectation by heat-kernel differentiation — independent of the closed form and of Itô	`bsV_satisfies_bs_pde_via_feynmanKac`
CRR → Black–Scholes	the n-step binomial call price converges to `S₀Φ(d₁) − Ke^{−rT}Φ(d₂)` (characteristic functions + Lévy continuity + put-call parity)	`binomialPrice_call_tendsto_bs_closed`
Continuous-time Itô formula	`f(B_T) − f(B_0) = ∫₀ᵀ f′(B_s) dB_s + ½∫₀ᵀ f″(B_s) ds`, on a from-scratch L² Itô integral, for a general `C³` `f` with no growth bound	`ito_formula_unrestricted`
The EMM via Girsanov	the risk-neutral measure is constructed as an explicit density change of the physical measure, `Q = withDensity(exp(−θX_T − ½θ²T))`; the discounted stock is a proven `Q`-martingale — retiring the Wald shortcut	`bs_discounted_isQMartingale`
Jump risk is never free	the Merton (1976) jump-diffusion price dominates Black–Scholes	`bsV_le_mertonCallPrice`

A theorem, up close

-- Coherent risk = sup of expected loss over the representing measures (the ADEH representation).
-- Closedness of the acceptance set is *derived* from the four axioms, not assumed.
theorem coherentRisk_isLUB {ι : Type*} [Fintype ι] [Nonempty ι] {ρ : (ι → ℝ) → ℝ}
    (hρ : IsCoherentRisk ρ) (X : ι → ℝ) :
    IsLUB ((fun q => ∑ i, q i * (- X i)) '' representingSet ρ) (ρ X)

-- Black–Scholes delta, in one line of the "magic identity" collapse: ∂V/∂S = Φ(d₁).
lemma hasDerivAt_bsV_S {K r σ : ℝ} (hK : 0 < K) (hσ : 0 < σ) {S τ : ℝ} (hS : 0 < S) (hτ : 0 < τ) :
    HasDerivAt (fun s => bsV K r σ s τ) (Phi (bsd1 S K r σ τ)) S

See MathFin/Examples.lean for a curated tour.

Status at a glance


theorems (machine-checked)	319
delivery-ready (`full` + `library_wrapper`)	304
full derivations	286
reduced cores (honest special cases)	15
placeholders / sorries	0
axioms used	`propext, Classical.choice, Quot.sound` only
Lean / Mathlib	`v4.31.0`, pinned (`lean-toolchain`)

Quick start

# Pull the pinned image (~3 min) instead of building locally (~15 min)
docker compose -f docker/docker-compose.yml pull verify

# Build the whole library — a clean exit means every theorem typechecks
docker compose -f docker/docker-compose.yml run --rm --entrypoint bash verify -lc 'lake build'

# Fast authoring loop (5–30s feedback via the persistent REPL daemon)
docker compose -f docker/docker-compose.yml up -d lean-repl
./scripts/lean-check.sh MathFin/<Section>/<Module>.lean

See CONTRIBUTING.md for the full workflow.

How verification works

The build is the proof. lake build re-elaborates every theorem against the pinned toolchain; a clean exit is the canonical verification.
Axiom audit. AxiomAudit.lean (headliners) and AxiomAuditGen.lean (generated over the whole corpus) pin #print axioms as #guard_msgs build invariants — no sorry, no project-local axioms.
Verification ledger. verification_ledger.json records the input-hash (snippet + transitive imports + toolchain pins) each entry last verified under; only entries whose inputs changed re-run.
CI gates. Every push runs the Python gates (status taxonomy, forbidden tactics, ledger freshness) and the environment linter before the Lean build.
Values review. Sessions that change proof content close with a multi-agent review over eight judgment lenses, logged in docs/values-review.md (cadence CI-enforced).

What's covered

A breadth-and-depth library across eleven areas. Headlines per area (full per-theorem audit + status in docs/coverage.md):

Black–Scholes & exotics — the full Greek matrix (δ, γ, vega, θ, ρ, vanna, volga, charm), digitals, BS-Merton dividends, Garman–Kohlhagen FX, implied-vol uniqueness, the PDE, Breeden–Litzenberger; Margrabe exchange, chooser, capped/bull/butterfly, lookback, Asian bounds.
Bachelier & Black-76 — arithmetic-BM pricing + Greeks; the futures-options formula + swaption.
Binomial / lattice — replication + uniqueness, American/Bermudan via the Snell envelope, CRR → Black–Scholes convergence, Merton 1973 dominance, André's reflection principle.
Fixed income & credit — bonds, duration/convexity, Redington immunization, yield-curve bootstrap, reduced-form hazard credit, Vasicek (ODE + SDE law), KMV–Merton default.
Portfolio & performance — Markowitz (2- and N-asset), CAPM + equilibrium, two-fund separation, risk parity, Black–Litterman, tangency; Sharpe/Sortino/Treynor/Information ratios, Kelly.
Risk measures — Gaussian VaR/CVaR closed forms, the coherent (ADEH) axioms + the representation as a sup over measures, spectral measures, Rockafellar–Uryasev, Herfindahl–Hirschman.
Stochastic foundations — the Itô tower (from-scratch L² integral, isometry, quadratic variation, Itô's formula), the FTAP tower (finite-Ω multi-period, general-Ω one-period, d-asset), static Girsanov, Feynman–Kac, and the convex-duality unification.
Actuarial & DeFi — Gompertz mortality, annuities, net premium; constant-product (Uniswap-v2) AMMs.

Scope: what's not done

Honesty is the point, so the gaps are explicit:

15 reduced_core entries — special cases or algebraic/structural cores whose fully general form is not yet formalized (the 2-D Itô formula, Lévy's characterisation, the fully-general L²/progressive Girsanov under Novikov, some Markov/Poisson cores). Tracked per-entry in docs/coverage.md.
SDE existence + uniqueness — existence is the Picard fixed point in the predictable L² space E (conditional on the small-horizon contraction); uniqueness (Theorem 8.2.5) is now full, derived via the L²-energy Grönwall argument (IsL2SolutionPair.uniqueness).
Girsanov (I↔II) — the bounded case is closed — the EMM/change-of-measure martingale side is proved, and the distributional Girsanov is now fully closed for bounded predictable θ — the honest domain of the Itô L² integral: Btheta_isQBrownianMotion_predictable shows B^θ_u = B_u + ∫₀ᵘθ ds is a Q-Brownian motion (zero start, Gaussian increments N(0, t−s), and independent disjoint increments) under Q = withDensity(exp(−∫₀ᵀθ dB − ½∫₀ᵀθ² ds)), dropping the path-continuity of the earlier bounded-adapted-continuous case (Btheta_isQBrownianMotion_adapted). The route is spine-free: the simple-θ exponential-martingale identity is passed to the limit through an a.e.-subsequence set-integral engine — no continuous stochastic-exponential-is-a-martingale (Novikov) crux and no adapted-integrand Itô formula. This is the culmination of the constant → simple → continuous-adapted → predictable arc; only the fully-general L²/progressive-θ (Novikov, unbounded) case remains open. The numéraire (IV↔I) bridge is wired (changeOfNumeraire + its BS-stock / Margrabe-S² / Kelly-EMM instances).
Known upstream/limit gaps — e.g. the superhedging strong-duality equality needs a finite-dimensional Farkas / polyhedral-cone closedness absent from Mathlib at this pin (#39).

The frontier is in the open issues and docs/roadmap.md.

Documentation

File	Contents
`docs/mathematical-architecture.md`	The field's spine — the four pillars, the connective bridges, and which seams are wired vs open.
`docs/architecture.md`	The engineering design: structural-principle modules, the three honesty tiers, the bridge methodology.
`docs/blueprint.md`	The deductive spine — a dependency graph from Brownian motion to Black–Scholes, each node linked to its proof.
`docs/coverage.md`	Per-theorem audit: faithfulness status, verification evidence, claim wording.
`docs/roadmap.md`	Strategic depth-vs-breadth framing and the tactical phase log.
`docs/values-review.md`	The judgment layer: the eight review lenses and the upgrade log.
`docs/bridges.md` · `docs/leaps.md` · `docs/patterns.md`	The Foundations→pricing bridges, the deductive leaps, and distilled Lean proof patterns.

Contributing · citation · license

Contributions welcome — see CONTRIBUTING.md and the good first issues. Please cite via the Zenodo DOI or the paper (CITATION.cff). Licensed under Apache 2.0.