Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalization of QFT

Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim

Abstract

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 theory, then describe our formalization and the design decisions that shaped it. We also explain the methods we used, including coding assistants, and conclude by considering how AI assisted formalization may influence the future of theoretical physics. Our original release assumed three results, Minlos' theorem, the nuclear property of Schwartz space, and Goursat's theorem. In subsequent releases from our group and from contributors from the Lean community, these assumptions have been proven (or avoided), so that the OS/GJ axioms are now proven using only Lean and its library Mathlib.

Formalization of QFT

Abstract

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 theory, then describe our formalization and the design decisions that shaped it. We also explain the methods we used, including coding assistants, and conclude by considering how AI assisted formalization may influence the future of theoretical physics. Our original release assumed three results, Minlos' theorem, the nuclear property of Schwartz space, and Goursat's theorem. In subsequent releases from our group and from contributors from the Lean community, these assumptions have been proven (or avoided), so that the OS/GJ axioms are now proven using only Lean and its library Mathlib.
Paper Structure (34 sections, 2 theorems, 76 equations, 1 figure)

This paper contains 34 sections, 2 theorems, 76 equations, 1 figure.

Table of Contents

  1. Introduction
  2. What is formalization and why?
  3. ITP in the age of AI
  4. Comparing Styles of Reasoning in Physics and Mathematics
  5. Brief status report on rigorous QFT with respect to the Mass Gap Problem
  6. Related work
  7. Axiomatic QFT and Constructive Frameworks
  8. Introduction to the mathematics
  9. Details of the formalization
  10. Construction of Gaussian Free Field
  11. Schwartz Test Functions
  12. Motivation for the definitions
  13. Other infrastructure
  14. Methods
  15. Tips and common pitfalls
  16. ...and 19 more sections

Key Result

Theorem 4.1

Let $E$ be nuclear. If $\chi:E\to\mathbb C$ is continuous, positive definite, and normalized by $\chi(0)=1$, then there exists a unique Borel probability measure $\mu$ on $E'$ such that for all $f\in E$, Equivalently, every continuous positive-definite functional on a nuclear space is the Fourier transform (characteristic functional) of a unique probability measure on the continuous dual.

Figures (1)

  • Figure 1: PDA trained on FORML4 ( image from lu_process_driven_2024). PDA is aimed at statement autoformalization rather than proof translation; proof steps are included to let the Lean compiler provide process-level feedback when jointly compiling the statement and proof steps. In the depicted example, the statement parses but a proof-step error reveals an incorrect autoformalization, guiding refinement lu_process_driven_2024.)

Theorems & Definitions (6)

  • Remark 3.1: Schwartz functions vs compactly supported test functions
  • Remark 3.2: OS4 Ergodicity Statement
  • Remark 3.3: OS4 Clustering
  • Theorem 4.1: Minlos
  • Lemma B.1: Convolution polynomial decay
  • proof : Proof sketch of OS4 (polynomial clustering) for the massive GFF