Formalization of QFT

Interactive theorem proving with the Lean 4 theorem prover, Mathlib and AI coding assistants has recently become a powerful method for checking and developing rigorous mathematical proofs. In this talk we introduce the technology and survey recent works using it in mathematical physics. These include the construction of the free massive bosonic field and verification of the Osterwalder-Schrader axioms, and work in progress to formalize the OS reconstruction theorem, the construction of P(\phi)_2 theory, and the proof of the Yang-Mills mass gap at strong coupling. Joint work with Sarah Hoback, Anna Mei, Ron Nissim, Matteo Cipollina and Xi Yin.

In-person only, to be posted after the talk on https://www.youtube.com/@mathematicalpicturelanguag2715/videos