Résumé
In this talk, we will discuss the current state of the formalization of modern number theory in mathlib, the mathematical library of Lean. We will highlight recent advancements, key challenges that have been addressed, and the broader implications of this work. Additionally, we will explore future directions and potential applications, emphasizing how these developments contribute to the growing ecosystem of formalized mathematics.
Riccardo Brasca
Riccardo Brasca obtained his Ph.D from the Università di Milano (Italy) in 2012, with a dissertation focused on p-adic modular forms. Following his doctoral studies, he did two postdocs at the Max Planck Institute for Mathematics in Bonn and the École Normale Supérieure in Lyon. Since 2013, he has been a "maître de conférences" at Université Paris-Cité.
