BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:AI for Formal Math\, and Physics\, and why they're different [Conf
 irmed]
DTSTART:20260415T150000Z
DTEND:20260415T163000Z
DTSTAMP:20260510T134400Z
UID:indico-event-2252@events.perimeterinstitute.ca
DESCRIPTION:Speakers: Alexander Meiburg (Perimeter Institute for Theoretic
 al Physics)\n\nAs little as five years ago\, the image of 'AI for Math' fo
 cused on specialty models that could discover interesting examples or con
 structions\, for example\, graphs with interesting parameters\, where our 
 intuition might be lacking but computer checking is simple. With large la
 nguage models this has flipped: AI can now generate English proofs with n
 ovel ideas and often human-like intuition\, but they are prone to tiny err
 ors that computers cannot catch. I'll discuss how Interactive Theorem Pro
 ving software is reshaping this\, where LLMs can ground their reasoning i
 n rigorous verification. I will discuss both how these models are develope
 d\, what they find easy or hard\, and what is required to apply this to t
 he domain of physics as opposed to pure math -- in particular\, why defin
 itions\, not proofs\, are increasingly the obstacle to AI-assisted physics
 .\n\nhttps://events.perimeterinstitute.ca/event/2252/
LOCATION:PI/4-405 - Bob Room (Perimeter Institute for Theoretical Physics)
URL:https://events.perimeterinstitute.ca/event/2252/
END:VEVENT
END:VCALENDAR