The Fundamental Theorem of Asset Pricing, Formalized in Lean 4

Battle Count: 75

The FTAP is the theoretical cornerstone of all arbitrage-free pricing, which underpins derivative valuation, risk-neutral pricing, and no-arbitrage bounds used in quantitative trading. However, this paper is a formal verification exercise rather than a practical trading tool. Its direct relevance to day-to-day quantitative trading is limited: it does not produce trading signals, pricing algorithms, or risk models. Its value is foundational—ensuring the mathematical underpinnings of pricing theory are rigorously correct. The variational construction (softplus potential, logistic density) could inspire computational approaches to finding risk-neutral measures in practice, but the paper does not develop this direction. The explicit formula for the EMM density (logistic weight) is potentially useful for numerical implementations.

Implementing the formalization requires deep expertise in Lean 4, Mathlib's measure theory, convex analysis, and finite-dimensional separation lemmas. The variational construction involves differentiating under the integral sign, coercivity arguments on orthogonal complements, and change-of-measure bookkeeping. For a practitioner wanting to use the results computationally, the mathematical content (softplus potential, logistic density, gains kernel) is straightforward, but the formal proof infrastructure is highly specialized. The three settings range from elementary (finite-state geometry) to moderately complex (d-asset variational construction). No external data pipelines or ML training are involved.

Extremely high reproducibility. The Lean toolchain is pinned at v4.31.0, Mathlib at revision fabf563a, and BrownianMotion at d6f23da. All theorems are sorry-free with axioms pinned to Mathlib's classical defaults (choice, propositional extensionality, quotient soundness) via a build-enforced axiom-audit gate using #print axioms. A verification ledger records hashes of exact sources. A plain 'lake build' from a clean checkout is the canonical check. The full artifact is publicly available on GitHub under Apache 2.0 licence.