Formalization of QFT
formal-verificationlean4quantum-field-theoryinteractive-theorem-provingai-assisted-formalization
Abstraction: Lean 4 machine-checked proof of free bosonic quantum field theory axioms
Key points:
- Formalizes the construction of free bosonic QFT in 4D Euclidean spacetime and its proof of Glimm-Jaffe (Osterwalder-Schrader) axioms using Lean 4 interactive theorem prover
- Initially assumed three auxiliary results (Minlos' theorem, nuclear property of Schwartz space, Goursat's theorem); all subsequently proved by the group and Lean community contributors
- AI coding assistants were used throughout the development process
- Proof of concept that extended arguments in mathematical physics can be translated into machine-checked proofs with existing AI tools
- Discusses how AI-assisted formalization may influence the future of theoretical physics research
- Michael R. Douglas et al. (2026); uses Lean's Mathlib library
Connections: Lean · Michael Douglas · Formal Verification · Interactive Theorem Proving · Quantum Field Theory · AI Assisted Proof
Source: https://arxiv.org/abs/2603.15770