Formalization of QFT: Osterwalder–Schrader Axioms for the Free Field in Lean 4

A foundational result in constructive quantum field theory is the construction of the free bosonic field on four-dimensional Euclidean spacetime and the verification that it satisfies the Glimm-Jaffe axioms, a variant of the Osterwalder-Schrader axioms. We present a complete formalization of this result in the Lean 4 interactive theorem prover. The project serves as a proof of concept that extended arguments in mathematical physics can be translated into machine-checked proofs using currently available formalization tools and AI assistance. We introduce the relevant background in interactive theorem proving and constructive quantum field theory, describe the structure of the formalization, and discuss the design choices and methods that made the project feasible. Because the work was carried out during a period of rapid change in AI coding capabilities, from July 2025 to March 2026, we also reflect on how these changes affected the formalization process. We conclude by discussing practical strategies for AI-assisted formalization and its possible role in the future of theoretical physics.