pith. sign in

arxiv: 2606.28990 · v1 · pith:2NR2OLQHnew · submitted 2026-06-27 · 💱 q-fin.MF

The Fundamental Theorem of Asset Pricing, Formalized in Lean 4

Raphael Coelho This is my paper

Pith reviewed 2026-06-30 08:28 UTC · model grok-4.3

classification 💱 q-fin.MF
keywords fundamental theorem of asset pricingequivalent martingale measureno arbitrageLean 4formal verificationconvex potentialone-period marketseparating hyperplane
5
0 comments X

The pith

A market is arbitrage-free exactly when it admits an equivalent martingale measure, now machine-checked in Lean 4 for three concrete settings.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes the Fundamental Theorem of Asset Pricing by formalizing its statement and proof in Lean 4 across a finite-state finite-horizon market, a one-period scalar-return market, and a one-period market with d assets. In the d-asset case it supplies an explicit construction: the equivalent measure arises as the minimizer of the convex potential E[log(1 + exp(<θ, Y>))], where absence of arbitrage is exactly the coercivity of this potential and the first-order condition at the minimizer yields the martingale property. The logistic weight attached to that minimizer supplies the density. A sympathetic reader cares because the formalization replaces abstract separation arguments with direct convex optimization and removes the possibility of overlooked gaps that can appear in pen-and-paper proofs.

Core claim

In the d-asset one-period setting the equivalent martingale measure is obtained explicitly as the minimizer of the smooth convex potential E[log(1 + e^{<θ,Y>})]; absence of arbitrage is precisely the coercivity of this potential, its first-order condition is the martingale property, and the minimizer's logistic weight is the density of the measure. The finite-state case reduces to geometry of a separating hyperplane and the scalar one-period case to an elementary change of measure. All three statements are proved inside Lean over Mathlib without Hahn-Banach, L^0-closedness, measurable selection, or non-redundancy assumptions, and every theorem is free of sorry.

What carries the argument

The smooth convex potential E[log(1 + exp(<θ, Y>))] whose minimizer produces the density of the equivalent martingale measure.

If this is right

  • Absence of arbitrage is equivalent to coercivity of the potential function.
  • The first-order optimality condition at the minimizer is exactly the martingale property.
  • The logistic weight of the minimizer supplies the Radon-Nikodym density of the equivalent measure.
  • The equivalence holds without any non-redundancy hypothesis on the assets.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The explicit convex-potential route may extend to multi-period discrete models where the usual separating-hyperplane arguments become cumbersome.
  • Because the construction is fully constructive inside Lean, one can mechanically generate the measure for any concrete finite market by running the minimization.
  • The same potential may serve as a computational proxy for arbitrage detection in numerical implementations that stay close to the formalized statement.

Load-bearing premise

The Lean code faithfully encodes the definitions and statements of arbitrage and equivalent martingale measure taken from the Harrison-Pliska and Föllmer-Schied literature.

What would settle it

An explicit finite or one-period market in which the formalized theorem asserts an equivalent martingale measure exists yet a direct calculation shows arbitrage is still possible, or vice versa.

Figures

Figures reproduced from arXiv: 2606.28990 by Raphael Coelho.

Figure 1
Figure 1. Figure 1: The three settings formalized here (solid) and the general multi-period theorem that [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
read the original abstract

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\theta,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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper formalizes the Fundamental Theorem of Asset Pricing (FTAP) in Lean 4 over Mathlib in three settings: the finite-state finite-horizon case (Harrison-Pliska), the one-period scalar-return case (Föllmer-Schied), and the one-period d-asset case. In the d-asset setting it gives an explicit construction of the equivalent martingale measure as the minimizer of the smooth convex potential E[log(1 + e^{<θ,Y>})], with no-arbitrage equivalent to coercivity of the potential, the first-order condition equivalent to the martingale property, and the logistic weights supplying the density. The development is sorry-free, axioms are pinned to Mathlib classical defaults via build gates, and the general multi-period Dalang-Morton-Willinger theorem is explicitly excluded.

Significance. If the formalization holds, the work supplies the first machine-checked version of FTAP in any proof assistant, together with an explicit convex-potential construction that avoids Hahn-Banach, L^0-closedness, measurable selection, and non-redundancy assumptions. The reproducibility from a pinned toolchain and the explicit boundary conditions are additional strengths that lower the barrier to further formalizations in mathematical finance.

minor comments (2)
  1. The abstract and §1 could usefully include a one-sentence pointer to the precise Mathlib files or module names that contain the three headline theorems, to help readers locate the code immediately.
  2. Notation for the inner product ⟨θ,Y⟩ and the logistic weight is introduced in the d-asset section; a short table collecting all symbols used across the three settings would improve readability for readers who consult only one case.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript, the clear summary of its contributions, and the recommendation to accept. No major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper is a machine-checked formalization of the FTAP in Lean 4 against the external Mathlib library. The three settings encode standard statements from Harrison-Pliska and Föllmer-Schied literature. The d-asset construction defines the potential E[log(1+e<θ,Y>)] independently, proves coercivity iff no arbitrage, derives the martingale property from the FOC, and obtains the density from the logistic weight; all steps are explicit Lean theorems with no fitted parameters, no self-citation chains, and no reduction of the claimed equivalence to its own inputs. The boundary (exclusion of multi-period DMW) is stated explicitly. This is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on Mathlib's standard axioms for classical mathematics and probability; no free parameters or new entities are introduced by the paper.

axioms (1)
  • standard math Mathlib's axioms for classical mathematics and probability theory
    The paper pins the development to Mathlib's classical defaults via a build gate.

pith-pipeline@v0.9.1-grok · 5788 in / 1240 out tokens · 61051 ms · 2026-06-30T08:28:24.521438+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

14 extracted references · 4 canonical work pages · 2 internal anchors

  1. [1]

    J. M. Harrison, D. M. Kreps. Martingales and arbitrage in multiperiod securities markets. Journal of Economic Theory, 20(3):381–408, 1979

    1979

  2. [2]

    J. M. Harrison, S. R. Pliska. Martingales and stochastic integrals in the theory of continuous trading.Stochastic Processes and their Applications, 11(3):215–260, 1981

    1981

  3. [3]

    R. C. Dalang, A. Morton, W. Willinger. Equivalent martingale measures and no-arbitrage in stochastic securities market models.Stochastics and Stochastic Reports, 29(2):185–201, 1990

    1990

  4. [4]

    Delbaen, W

    F. Delbaen, W. Schachermayer. A general version of the fundamental theorem of asset pricing.Mathematische Annalen, 300(1):463–520, 1994

    1994

  5. [5]

    Föllmer, A

    H. Föllmer, A. Schied.Stochastic Finance: An Introduction in Discrete Time, 4th ed. De Gruyter, 2016

    2016

  6. [6]

    de Moura, S

    L. de Moura, S. Ullrich. The Lean 4 theorem prover and programming language. In CADE 28, LNCS 12699, pp. 625–635, 2021

    2021

  7. [7]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. InCPP 2020, pp. 367–381, 2020. 8

    2020

  8. [8]

    R. Coelho. A formally verified library of mathematical finance in Lean 4. arXiv:2606.01356, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  9. [9]

    R. Coelho. A machine-checked Itô calculus for Brownian motion. arXiv:2606.15089, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  10. [10]

    Echenim, H

    M. Echenim, H. Guiol, N. Peltier. Formalizing the Cox–Ross–Rubinstein pricing of European derivatives in Isabelle/HOL.Journal of Automated Reasoning, 64:737–765, 2020

    2020

  11. [11]

    A. Keskin. A formalization of martingales in Isabelle/HOL. arXiv:2311.06188, 2023

    work page arXiv 2023

  12. [12]

    Avigad, J

    J. Avigad, J. Hölzl, L. Serafin. A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389–423, 2017

    2017

  13. [13]

    Degenne, D

    R. Degenne, D. Ledvinka, E. Marion, P . Pfaffelhuber. Formalization of Brownian motion in Lean. arXiv:2511.20118, 2025

    work page arXiv 2025

  14. [14]

    Degenne et al.brownian-motion: a Lean 4 development of Brownian motion

    R. Degenne et al.brownian-motion: a Lean 4 development of Brownian motion. https: //github.com/RemyDegenne/brownian-motion, 2024–2026. 9

    2024