Pith. sign in

REVIEW 2 minor 14 references

The Fundamental Theorem of Asset Pricing, Formalized in Lean 4

T0 review · 0 major / 2 minor · reviewed 2026-06-30 · grok-4.3

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

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

desk verdict This is the first machine-checked FTAP in Lean, with a clean explicit convex-potential construction for the d-asset case that stays elementary. read the letter →

arxiv 2606.28990 v1 pith:2NR2OLQH submitted 2026-06-27 q-fin.MF

Raphael Coelho This is my paper · ORCID
classification q-fin.MF
keywords fundamentaltheoremofassetpricingequivalentmartingalemeasurenoarbitrageLean4formalverificationconvexpotentialone-periodmarketseparatinghyperplane
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

What carries the argument

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

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.

Watch

Extended reading notes

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.

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.

Editorial extensions

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.

Reading between the lines

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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

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 · score 0.0 of 10

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.

Assumptions & free parameters 0 free parameters · 1 assumptions · 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.

assumptions (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.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Fundamental Theorem of Asset Pricing, Formalized in Lean 4." pith.science (2026). https://pith.science/paper/2NR2OLQH

@misc{pith2026260628990,
  author       = {Pith},
  title        = {Pith review of: The Fundamental Theorem of Asset Pricing, Formalized in Lean 4},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2NR2OLQH}},
  note         = {Machine review of arXiv:2606.28990}
}
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.

Figures

Figures reproduced from arXiv: 2606.28990 by the authors.

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 ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

  1. [1]

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

    work page 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

    work page 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

    work page 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

    work page 1994

  5. [5]

    Föllmer, A

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

    work page 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

    work page 2021

  7. [7]

    The Lean mathematical library

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

    work page 2020

  8. [8]

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

    work page Pith review arXiv 2026

Show all 14 references
  1. [9]

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

    2026 arXiv

  2. [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

  3. [11]

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

    2023

  4. [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

  5. [13]

    Degenne, D

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

    2025

  6. [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

Pith tools

Reviewed June 30, 2026 · model on record in the stance chip above.