BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Michael Douglas (Harvard University)
DTSTART:20260506T190000Z
DTEND:20260506T200000Z
DTSTAMP:20260513T133453Z
UID:MathPic/147
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/MathPic/147/
 ">Formalization of QFT</a>\nby Michael Douglas (Harvard University) as par
 t of Mathematical Picture Language Seminar\n\nLecture held in Jefferson 36
 8.\n\nAbstract\nInteractive 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 fiel
 d and verification of the Osterwalder-Schrader axioms\, and work in progre
 ss to formalize the OS reconstruction theorem\, the construction of P(\\ph
 i)_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.\n
LOCATION:https://researchseminars.org/talk/MathPic/147/
END:VEVENT
END:VCALENDAR