quant research // summarizing the paperLOADING
Raphael Coelho · 2026-06-27
The authors take a cornerstone result of financial math — that a market has no arbitrage exactly when a certain 'martingale measure' exists — and encode it in the Lean 4 proof assistant so a computer can verify every step. They cover three simpler settings (finite-state, one-period scalar, and one-period multi-asset), and for the multi-asset case they build the martingale measure explicitly by minimizing a smooth convex function. They claim this is the first machine-checked proof of this theorem in any proof assistant.
Why it matters: This is foundational math verification, not a trading strategy, so its direct relevance to day-to-day investing is minimal. The main value is theoretical rigor: it confirms the logical scaffolding beneath no-arbitrage pricing that underpins derivative valuation and risk-neutral modeling.
⚠ This is a formal mathematics/verification paper with no data, backtests, or trading application, and it deliberately omits 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.