Osterwalder–Schrader axioms for the Gaussian free field: a machine-checked proof in every dimension
 

The Osterwalder–Schrader axioms are five conditions on a probability measure on the space S′(ℝᵈ) of tempered distributions, from which one can reconstruct a quantum field theory — a Hilbert space carrying a unitary representation of the Poincaré group. They are what makes Wick rotation a theorem rather than a formal manipulation.

I will explain what the five conditions ask for in analytic terms, construct the massive Gaussian free field as a measure on S′(ℝᵈ) via Minlos' theorem on the nuclear space S(ℝᵈ), and outline the proof, following Glimm and Jaffe, that it satisfies all of them. Reflection positivity, the one axiom with real content, I will prove in full, using nothing beyond the Schur product theorem for positive-definite kernels.

We have formalized all of it in Lean 4 — the construction of the measure and the proofs of all five axioms. Every step, from the nuclearity of S(ℝᵈ) through Minlos' theorem, is machine-checked, and depends on nothing beyond the three foundational axioms of Lean's logic. Working out which properties of the covariance (−Δ + m²)⁻¹ the proofs actually use reduced them to two (an exponentially weighted L¹ bound and one Fourier identity) and let us remove a restriction on the dimension that proved to be an artifact of an estimate rather than a feature of the mathematics, giving the result uniformly for every d ≥ 2. I will close with what machine verification does and does not certify.

No background in quantum field theory or in formal verification will be assumed.

Joint work with Michael R. Douglas, Sarah Hoback, Anna Mei and Ron Nissim. 
The library is at https://github.com/mrdouglasny/OSforGFF; 
the result is registered last Monday in the Palomar registry as PALOMAR-2026-08-31-000012.