{"id":"arxiv/2603.15770","url":"https://arxiv.org/abs/2603.15770","tags":["hep-th","cs.LO","math-ph"],"score":0,"title":"Formalization of QFT","domain":"hep-th","source":"arxiv","authors":["Michael R. Douglas","Sarah Hoback","Anna Mei","Ron Nissim"],"reviews":0,"subject":"hep-th","summary":"A foundational result in constructive quantum field theory is the construction of the free bosonic quantum field theory in four-dimensional Euclidean spacetime and the proof that it satisfies the Glimm-Jaffe axioms, a variant of the Osterwalder-Schrader axioms. We present a formalization of this result in the Lean 4 interactive theorem prover. The project is intended as a proof of concept that extended arguments in mathematical physics can be translated into machine-checked proofs using existing AI tools. We begin by introducing interactive theorem proving and constructive quantum field…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-03-16","reactions":{}}