Automath! On the Origin of False Proofs by Means of Bugs in Proof Assistants, Yannick Foster

Organisé par

ENS Paris

| 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.…

Conférence de mathématiques à Paris, le vendredi 16 octobre 2026, de 10:30 à 11:30. Organisée par ENS Paris. Lieu : Institut Henri Poincaré amphithéâtre Hermite. Entrée gratuite (inscription parfois demandée). En anglais.

+ Ajouter à Google Agenda

Vérifie les horaires sur la page officielle avant de te déplacer.