Three Proofs for a Lean Math-Finance Library
formal-mathfin is a Lean 4 library that states results from mathematical finance and proves them. Between September and October 2026 I had three pull requests merged there. Each one takes a textbook model and checks, line by line, what the textbook claims about it.
Lean also exposes the cases the textbook skips. In two of the three PRs, those cases turned out to be the most interesting part of the work.
Glosten–Milgrom: when the spread is positive
PR #211, merged 2026-09-09.
In the Glosten–Milgrom model (1985), a market maker quotes a bid and an ask without knowing whether the asset is worth V_H or V_L. Some traders do know. The market maker sets each quote at the asset's expected value given that someone chose to trade at it. A buy is evidence the value is high, so the ask sits above the bid. The spread is the price of trading against better-informed people.
That ties back to an earlier post here: who you trade against, and what they know, shapes the price you get.
The issue (#107) asked for a proof that the spread is positive whenever some traders are informed (p > 0) and V_L < V_H. As stated, that is false. If the prior probability θ of the high value is exactly 0 or 1, everyone already knows the value and the spread is zero. Worse, at θ ∈ {0, 1} with p = 1, one side of the market never trades. The conditional probability is then undefined and evaluates to 0 in Lean. A careless proof would still compile.
So the theorem carries the missing hypothesis 0 < θ < 1. The broken corners are stated as theorems of their own, not left to prose. A non-vacuity witness shows the hypotheses can all hold at once, and p ≤ 1 is derived rather than assumed. The PR adds 37 theorems with no sorry, using only Lean's standard axioms.
The maintainer later fixed one docstring of mine that described the bad corner wrongly. The lesson I kept: a limit that lives only in the PR description doesn't reach the library. It has to be in the statement or the metadata.
A price with drift
PR #228, merged 2026-10-02.
The library modelled prices as a pure martingale: S = S₀ + ∫σ dB, all noise and no trend. #194 asked for a drift term, S = S₀ + ∫b ds + ∫σ dB, and for the gains of a strategy ψ against it.
The main theorem says the drift part of ∫ψ dS is, along each path, the ordinary integral ∫₀ᵀ ψ b ds. It lives in a new file, so nothing that depends on the original price moves.
Two details needed care. The product ψb must be square-integrable, and the usual condition on ψ doesn't guarantee that, so it is an explicit hypothesis. And where the volatility σ is zero but the drift isn't, the gains depend on an arbitrary choice of ψ. I raised it in the PR rather than hiding it, and the maintainer chose to keep the drift general.
CIR: the bond-price loadings
PR #245, merged 2026-10-15.
In the Cox–Ingersoll–Ross model, the short rate mean-reverts to θ at speed κ, with volatility σ√r. The zero-coupon bond price has the affine form
P(0, T) = exp(A(T) − B(T)·r₀)
and the loadings A and B have textbook closed forms. With γ = √(κ² + 2σ²):
B(T) = 2(e^{γT} − 1) / ((γ + κ)(e^{γT} − 1) + 2γ)
The claim is that B solves the Riccati equation B' = 1 − κB − ½σ²B² with B(0) = 0, and that A' = −κθB with A(0) = 0. The PR proves both, at every T, by differentiating the closed forms in Lean. The second proof needs σ ≠ 0, since A divides by σ².
This is the least surprising of the three: the textbook is right. Its value is that the formula is now checked, and stated in the form the library's planned general affine framework (#63) uses, so CIR can slot in as an instance.
More to come; formal-mathfin is an ongoing collaboration.