Machine-Checked Theorem Records and Formal-Proof Provenance

A machine-checked theorem proves exactly the proposition elaborated in a particular formal environment. To interpret it as a QFT result, one must retain the theorem declaration, definitions, source snapshot, dependency lock, trusted kernel, imported axioms, and the mathematical correspondence between encoded and physical objects. The four-dimensional massive Gaussian free field formalized in Lean is a concrete example: it verifies a substantial Euclidean theorem, but not an interacting continuum construction or Osterwalder–Schrader reconstruction itself.

Required background. Theorem-First Claim Records supplies the claim grammar; Domains, Signatures, Supports, and Regularity fixes the encoded function spaces; and Limits, Completeness, and Modes of Convergence distinguishes formal limits from informal notation. Helpful background. Exact Statements, Saddle Expansions, and Conditional Derivations provides the same scope discipline for non-formal exact claims.

What the kernel certifies

Lean elaborates a declaration into a term whose type is the proposition being proved. Its small trusted kernel checks that term against the constants and axioms already present in the environment. A successful check supports the implication

$$\text{imported declarations and axioms} \quad\vdash\quad \text{formal theorem type}.$$

It does not independently establish that a Lean definition correctly models a physical field, that a cited informal theorem has been encoded faithfully, or that a stronger natural-language paraphrase follows. The trusted base includes the kernel and foundational principles reported by the environment; build tooling, elaboration, native code, external solvers, generated source, and dependency retrieval add further reproducibility or supply-chain questions. Lean 4’s architecture and kernel-checked proof terms are described by de Moura and Ullrich de Moura and Ullrich 2021, §§ 2–5, pp. 627–633.

Three checks answer different questions.

• lake build asks whether the pinned project elaborates and compiles.
• #print axioms theoremName asks which axioms occur transitively in that theorem. The significant warning token is sorryAx; ordinary foundational constants such as quotient soundness, propositional extensionality, or classical choice must be interpreted according to the project’s accepted logic.
• Reading the theorem type and definitions asks whether the formal proposition is the mathematical statement of interest.

A project can build with sorry, with user-declared axioms, or with a weakened definition. Build success alone is therefore not a theorem inventory.

The encoded Gaussian field

Douglas, Hoback, Mei, and Nissim formalize a free massive bosonic field in four-dimensional Euclidean space following the probability-measure formulation in Glimm and Jaffe 1987, Chapter 6, pp. 89–90, with the formal development described in Douglas et al. 2026, §§ 3–4, pp. 10–15. At the source snapshot examined here, the principal objects are:

• Euclidean spacetime fixed to $\mathbb R^4$;
• real Schwartz test functions and tempered-distribution field configurations;
• a mass parameter $m\in\mathbb R$ with the typeclass assumption $0<m$;
• the covariance $(-\Delta+m^2)^{-1}$, represented through rigorously integrable position- and momentum-space formulas;
• a probability measure $\mu_{\mathrm{GFF}}(m)$ on tempered distributions, constructed using formalized nuclear-space and Minlos machinery;
• predicates called OS0 through OS4 in the repository’s Glimm–Jaffe-style formulation.

The master declaration is

theorem OSforGFF.gaussianFreeField_satisfies_all_OS_axioms
    (m : ℝ) [Fact (0 < m)] :
    SatisfiesAllOS (μ_GFF m)

and SatisfiesAllOS contains six fields: analyticity, regularity, Euclidean invariance, reflection positivity, clustering, and ergodicity. The source theorem is visible in OSforGFF/OS/Master.lean at the pinned snapshot, while the mathematical paper states the chosen axioms and its differences from the textbook formulation Douglas et al. 2026, § 3, pp. 10–12.

The encoded differences matter. The development uses Schwartz functions rather than only compactly supported tests. Its OS3 is the complex star formulation with positive-time support. Its OS4 conclusion includes a clustering predicate and an ergodicity predicate derived from a polynomial-clustering estimate. These are precise, valuable statements; they should not be renamed as whatever version of “the OS axioms” a different source happens to use.

For comparison, the original Euclidean axioms and reconstruction argument are stated by Osterwalder and Schrader 1973, §§ 2–4, pp. 86–103, and the corrected regularity conditions and reconstruction theorem appear in Osterwalder and Schrader 1975, §§ II–V, pp. 283–297. The Lean conjunction is interpreted by its definitions, not by assuming identity with either printed list.

Proof structure in the formal development

The construction follows a recognizable mathematical chain.

1. Positivity and continuity of the Gaussian characteristic functional, nuclearity of Schwartz space, and a formalized Minlos theorem construct $\mu_{\mathrm{GFF}}(m)$.
2. Fernique-type integrability and holomorphic differentiation establish the analytic generating functional used for OS0.
3. Plancherel and the bound $(p_E^2+m^2)^{-1}\leq m^{-2}$ give the OS1 regularity estimate.
4. Dependence of the covariance only on Euclidean distance gives OS2.
5. A mixed time–spatial representation writes the reflected covariance as a positive integral; a Schur–Hadamard argument lifts covariance positivity to the Gaussian generating functional, giving OS3.
6. Exponential covariance decay and Gaussian factorization give polynomial clustering; a variance estimate for time averages yields OS4 ergodicity.

Appendix B of the paper provides the informal proof sketches and identifies the corresponding formal ingredients Douglas et al. 2026, Appendix B, pp. 28–35. The original release assumed Minlos’ theorem, nuclearity of Schwartz space, and Goursat’s theorem. Later releases proved or avoided those assumptions; the paper records the change and retains an original branch for comparison Douglas et al. 2026, § 1.5 and § 4, pp. 8–15.

A reproducible snapshot and replay

The following record was checked on 10 August 2026. The source was cloned at commit 2f0965a42c90e66b55f8de9735c7e9e558fbe365, dated 8 August 2026. Its lean-toolchain pins leanprover/lean4:v4.33.0-rc1. Its lake-manifest.json pins, among other dependencies, Mathlib commit 79d0395a1825a6264ad5d269e35e60537518955e, GaussianField commit f2481cf3d6accc180b8ece629ac6b4681c1fe162, BochnerMinlos commit a5f46ec87477c666349408f6d77d43e3c0517355, and kolmogorov_extension4 commit 45b4694ce1f7cd0fb0f00079510cd83c94e35a68.

A clean machine with Git and elan can replay the environment without following a moving branch:

git clone https://github.com/mrdouglasny/OSforGFF.git
cd OSforGFF
git checkout 2f0965a42c90e66b55f8de9735c7e9e558fbe365
lake build

Then create a temporary Check.lean outside the tracked source tree:

import OSforGFF.OS.Master

#check OSforGFF.gaussianFreeField_satisfies_all_OS_axioms
#print OSforGFF.gaussianFreeField_satisfies_all_OS_axioms
#print axioms OSforGFF.gaussianFreeField_satisfies_all_OS_axioms

and run lake env lean /absolute/path/to/Check.lean. Preserve the complete command output, platform, toolchain version, commit, and manifest hash. Search the axiom report specifically for sorryAx and unexpected user axioms; do not summarize an empty custom-axiom list as “no foundations.” The checked snapshot’s source declaration and project description report no sorry proof terms and no custom axioms in the main theorem, while the dependency lock supplies the exact external code on which that report depends.

The replay is scientific evidence only for the pinned source and toolchain. A later main, a different manifest, or a locally edited file is a new formal object even when the same command exits successfully.

The licensed QFT claim

The theorem-to-physics map has a sharp ceiling.

Formal result	Narrow mathematical conclusion	Conclusion not supplied
construction of $\mu_{\mathrm{GFF}}(m)$	a probability measure on encoded tempered-distribution configurations for $m>0$ in $d=4$	an interacting measure or a massless construction
OS0 and OS1 fields of SatisfiesAllOS	the repository’s analytic and regularity predicates for its generating functional	every growth condition used in every OS reconstruction theorem
OS2 field	invariance under the encoded Euclidean group action	Lorentzian covariance before reconstruction
OS3 field	positivity of the encoded complex reflected form on the encoded positive-time class	positivity for a weaker or differently supported test class by name alone
OS4 fields	encoded clustering and ergodicity statements for the massive Gaussian measure	a general interacting mass-gap theorem
master conjunction	all listed predicates hold simultaneously for $\mu_{\mathrm{GFF}}(m)$	a formalized OS reconstruction, Wightman theory, Haag–Kastler net, Yang–Mills theory, or nontrivial interacting continuum limit

Thus the result rigorously strengthens the treatment of Regulated Bosonic Field Integrals: it replaces a heuristic infinite-dimensional Lebesgue measure by a constructed Gaussian probability measure and verifies its encoded Euclidean conditions. It does not license a claim that Lean has constructed interacting four-dimensional QFT.

Failure test: a build can preserve syntax while changing meaning

Two adversarial changes expose why the snapshot and definitions are indispensable.

Dependency change. Replace the manifest or run lake update. Even if the project builds, theorem elaboration now occurs against different definitions and proofs. The new run must record the new transitive revisions and re-run the axiom query. Reusing the old prose would incorrectly treat dependency-sensitive evidence as invariant.

Weakened reflection positivity. Replace the complex star formulation by a predicate over only real tests, omit complex conjugation, or shrink the positive-time class. The master theorem may become easier and still compile under the same English label OS3_ReflectionPositivity; it would prove a different proposition. This is not hypothetical bookkeeping: the repository history includes a 7 March 2026 correction upgrading OS3 to the complex star formulation. The current theorem must therefore be interpreted through the current source definition, not through the identifier’s name.

In either case, the strongest surviving claim is that the altered project proves its altered Lean proposition. The earlier mathematical interpretation is suspended until the new definitions, theorem type, dependency report, and reflection-positivity correspondence have been compared.

Independent checks

Mathematical reflection check. For a positive-time Schwartz function, independently derive the mixed representation

$$\langle\Theta f,C_m f\rangle = \int_{\mathbb R^3} \frac{d^3\mathbf p}{2\omega_m(\mathbf p)} \left\lvert \int_0^\infty e^{-\omega_m(\mathbf p)t} \widetilde f(t,\mathbf p)\,dt \right\rvert^2 \geq0.$$

This checks that the formal OS3 target has the expected free-field content.

Source check. Resolve the theorem identifier to its file, inspect the exact SatisfiesAllOS fields, and compare them with the paper’s § 3 remarks. An identifier without its definition is insufficient.

Dependency check. Hash lean-toolchain, lake-manifest.json, and the theorem file before and after replay. A mismatch identifies a different environment even if git status looks clean.

Axiom check. Run #print axioms on the master theorem and on any wrapper theorem used in prose. A clean inner theorem does not protect a wrapper that imports an additional assumption.

Nontriviality check. OS predicates alone can be vacuously satisfied by overly degenerate constructions. Inspect the separate nontriviality theorem and verify that some smeared field has strictly positive variance; do not infer it merely from the conjunction’s name.

Common pitfalls

Equating checked syntax with faithful modeling. The kernel verifies the encoded proposition. Human mathematical review is still needed for definitions and their correspondence to QFT.

Reporting “zero axioms” imprecisely. The meaningful statement is absence of sorryAx and undeclared project assumptions in the theorem’s transitive axiom report, within Lean’s stated foundations.

Citing a moving branch. A branch URL cannot reproduce a dated theorem. Cite a full commit and retain its manifest.

Exercises

1. Interpret an axiom report. Suppose #print axioms T lists propext, Classical.choice, and Quot.sound, but not sorryAx or a project-specific axiom. What may be concluded?

Solution

The proof term for T depends only on those accepted Lean foundational principles among the reported axioms; it does not contain an admitted proof through sorryAx and does not expose a named project assumption. This is not foundation-free mathematics, and it says nothing yet about whether the definitions faithfully encode the intended physical claim.

2. Remove reflection positivity. Define a structure identical to SatisfiesAllOS but without its OS3 field and prove the corresponding conjunction for the Gaussian measure. Can one claim OS reconstruction?

Solution

No. The new conjunction proves analyticity, regularity, invariance, clustering, and ergodicity in the encoded senses, but it supplies no positive reflected form. The Hilbert-space quotient in OS reconstruction therefore lacks its positivity input. Reusing the old theorem name or prose cannot restore the removed field.

3. Separate theorem replay from source inspection. Why are both lake build and #print axioms needed?

Solution

lake build verifies that the pinned project elaborates and compiles as a whole. It can still succeed when declarations use sorry or explicit axioms. #print axioms traces the assumptions of the particular theorem used in the claim. Neither command checks physical interpretation, so the theorem type and definitions must also be inspected.

References

• de Moura, Leonardo, and Sebastian Ullrich. “The Lean 4 Theorem Prover and Programming Language.” In Automated Deduction—CADE 28, Lecture Notes in Computer Science 12699, 625–635. Cham: Springer, 2021. DOI. Open PDF.
• Douglas, Michael R., Sarah Hoback, Anna Mei, and Ron Nissim. “Formalization of QFT.” arXiv:2603.15770 [hep-th] (2026). Abstract. Open PDF.
• Douglas, Michael R., Sarah Hoback, Anna Mei, and Ron Nissim. OSforGFF: A Lean 4 Formalization of the Gaussian Free Field in d=4 and Proof of the Osterwalder–Schrader Axioms. Snapshot 2f0965a42c90e66b55f8de9735c7e9e558fbe365, 8 August 2026. Source snapshot.
• Glimm, James, and Arthur Jaffe. Quantum Physics: A Functional Integral Point of View. 2nd ed. New York: Springer, 1987. DOI.
• Osterwalder, Konrad, and Robert Schrader. “Axioms for Euclidean Green’s Functions.” Communications in Mathematical Physics 31 (1973): 83–112. DOI. Open PDF.
• Osterwalder, Konrad, and Robert Schrader. “Axioms for Euclidean Green’s Functions II.” Communications in Mathematical Physics 42 (1975): 281–305. DOI. Open PDF.