BEGIN:VCALENDAR
VERSION:2.0
X-WR-CALNAME;VALUE=TEXT:Michael Douglas (Harvard): Formalization of QFT
PRODID:-//Harvard events data//EN
BEGIN:VEVENT
UID:event_1893606_0
SUMMARY:Michael Douglas (Harvard): Formalization of QFT
DESCRIPTION:<p>Speaker: Michael Douglas</p><p>Title: <span>Formalization of QFT</span></p><p><span>Abstract: 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.&nbsp; In this talk we introduce the technology and survey recent works using it in mathematical physics.&nbsp; 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.&nbsp; Joint work with Sarah Hoback, Anna Mei, Ron Nissim, Matteo Cipollina and Xi Yin.</span></p>
LOCATION:Jefferson 368 
STATUS:CONFIRMED
DTSTART:20260506T190000Z
DTEND:20260506T200000Z
END:VEVENT
END:VCALENDAR