Prof. Riccardo Brasca
Institut de Mathématiques de Jussieu-Paris Rive Gauche
Around Formalization: Why and How to Explain Mathematics to a Computer
Tuesday, May 5th, 2026 - 16:30
Room 1A150 Torre Archimede
--- > Click here to register, if you plan to attend, for organizational reasons <---
Formalization means using a computer not merely to carry out calculations, but to check and follow mathematical reasoning. It is becoming a powerful new tool for research mathematicians. Today, even recent mathematical results can be formalized in a reasonable amount of time, and this is likely to improve significantly in the coming years. In this talk, I will present the process of formalization through a range of examples, and explain why it can be useful for mathematics in the ordinary sense of the word. No prerequisites are required. I will also cover some of the latest developments in AI and how they are beginning to transform the practice of formalization.
Short Bio
Riccardo Brasca is a Maître de conférences (tenured associate professor) at Université Paris Cité and a member of the Institut de Mathématiques de Jussieu–Paris Rive Gauche. His research focuses on number theory and the formalization of mathematics. He is a scientific coordinator of the ANR project FALSE and an active contributor to the Lean theorem prover and its mathematical library mathlib, where he serves as a maintainer. He coordinated the formalization of Fermat’s Last Theorem for regular primes in Lean and contributed to the Liquid Tensor Experiment.
He previously held postdoctoral positions at ENS Lyon and at the Max Planck Institute for Mathematics, and completed his PhD at the Università degli Studi di Milano under the supervision of Fabrizio Andreatta.For further details, please refer to the official website.