quant research // summarizing the paperLOADING
Raphael Coelho · 2026-06-27
The paper takes a cornerstone of finance theory — that a market has no arbitrage exactly when a special 'martingale' probability measure exists — and proves it rigorously inside the Lean 4 computer proof assistant. It covers three simpler cases (finite states, a one-period single-return market, and a one-period multi-asset market) and, for the multi-asset case, builds the pricing measure explicitly by minimizing a smooth convex function. The authors claim this is the first fully machine-checked proof of this theorem, and it deliberately stops short of the general multi-period case.
Why it matters: This is foundational mathematics rather than a tradable strategy, so its direct relevance to day-to-day investing is minimal. It matters mainly to those building or verifying pricing and risk models where mathematical correctness is critical, since machine-checked proofs reduce the risk of subtle theoretical errors.
⚠ This is a pure theoretical/formal-verification result with no empirical data, trading application, or coverage of the general multi-period case.
The Fundamental Theorem of Asset Pricing states that a market is free of arbitrage exactly when it admits an equivalent martingale measure. We formalize it in Lean 4 over Mathlib in three settings: a finite-state market over a finite horizon (Harrison-Pliska), a one-period market on an arbitrary probability space with a single scalar return (Follmer-Schied), and a one-period market with finitely many assets. The finite case is the geometry of a separating hyperplane; the scalar one-period case is an elementary change of measure. In the $d$-asset case the equivalent martingale measure is constructed explicitly, as the minimiser of the smooth convex potential $\mathbb{E}[\log(1+e^{\langleθ,Y\rangle})]$: absence of arbitrage is precisely coercivity of the potential, its first-order condition is the martingale property, and the minimiser's logistic weight is the density of the measure. The construction uses no Hahn-Banach theorem, no $L^0$-closedness argument, no measurable selection, and no non-redundancy hypothesis. To our knowledge this is the first machine-checked Fundamental Theorem of Asset Pricing in any proof assistant. The boundary is explicit: the general multi-period Dalang-Morton-Willinger theorem lies outside the development. Every theorem is sorry-free, each headline result's axioms are pinned to Mathlib's classical defaults by a build-enforced gate, and the whole is reproducible from a pinned toolchain.
Go deeper: a full research-committee breakdown of this paper, its assumptions and failure modes, and how its method would apply to a specific ticker or your watchlist. See StockTools AI →
AI summary generated from the paper’s public abstract via arXiv; it may miss nuance — read the source before relying on it. Thank you to arXiv for its open-access interoperability; StockTools is not affiliated with arXiv, and all rights remain with the authors. Educational only, not financial advice.