Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
Open to all
-

Abstract

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

Riccardo Brasca a obtenu son doctorat à l'université de Milan (Italie) en 2012, avec une thèse portant sur les formes modulaires p-adiques. Après son doctorat, il a effectué deux postdoctorats, l'un au Max-Planck-Institut für Mathematik à Bonn et l'autre à l'École normale supérieure de Lyon. Depuis 2013, il est maître de conférences à l'université Paris-Cité et depuis 2020 il travaille en formalisation des mathématiques.

Speaker(s)

Riccardo Brasca

Senior Lecturer, Université Paris Cité