BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Département de mathématiques et applications - ECPv6.2.2//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Département de mathématiques et applications
X-ORIGINAL-URL:https://www.math.ens.psl.eu
X-WR-CALDESC:évènements pour Département de mathématiques et applications
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20260329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20261025T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20261016T103000
DTEND;TZID=Europe/Paris:20261016T113000
DTSTAMP:20261016T014130
CREATED:20261005T080341Z
LAST-MODIFIED:20261005T080709Z
UID:22248-1792146600-1792150200@www.math.ens.psl.eu
SUMMARY:Automath! On the Origin of False Proofs by Means of Bugs in Proof Assistants\, Yannick Foster
DESCRIPTION:Proof assistants have entered mainstream mathematical discourse so fast that now they are almost silently accepted as the ultimate guardians of correct proofs. Both the recent forced Euler blowup result by Buckmaster and Alpöge and the solution to the Navier-Stokes problem announced by OpenAI come with proofs verified in the Lean proof assistant\, with code almost entirely written using LLMs. Only six months ago an experiment led by Tristan Stérin showed that LLMs are effective at finding bugs in proof assistants: several bugs were found both in Lean and the Rocq proof assistant. As a demonstration\, Ramana Kumar has published a proof of the Collatz Conjecture in Lean\, making use of a bug. These experiments have been followed by a flurry of bugs in Lean and Rocq found by Daniel Selsam at OpenAI. In this talk\, I will discuss the tension between proof assistants as guardians for LLM-coded proofs and as vulnerable target for LLM-guided bug search. In this talk I will discuss what a false proof is\, what a bug in a proof assistant is\, and give a genealogy of bugs that have been found this year\, focusing on what features of proof assistants they usually occur in. I will conclude with some thoughts on how we can have and increase trust in results developed in proof assistants.\n \n 
URL:https://www.math.ens.psl.eu/evenement/automath-on-the-origin-of-false-proofs-by-means-of-bugs-in-proof-assistants-yannick-foster/
LOCATION:Institut Henri Poincaré amphithéâtre Hermite
CATEGORIES:Séminaire Automath
END:VEVENT
END:VCALENDAR