Register for Lean for the Curious Mathematician 2026!

Hi! I am a Maître de conférences (= tenured associate professor) in the Department of Mathematics at Université Paris Cité, working in the automorphic forms group at the Institut de Mathématiques de Jussieu-Paris Rive Gauche. My main research interests are in formalization of mathematics and number theory. I am one of the scientific coordinators of the ANR project FALSE.

I am actively involved in the Lean project and its Mathematical Library mathlib, where I serve as a maintainer. I coordinated the project to formalize Fermat’s last theorem for regular primes in Lean and I also contributed to the Liquid Tensor Experiment. If you’re interested in trying your hand at formalizing mathematics, I recommend starting with the Natural Number Game. You might also enjoy exploring the Lean community blog.

I have been a post-doc at the ENS-Lyon under the supervision of Vincent Pilloni and at the Max Planck Institute for Mathematics. I completed my PhD in March 2012 under the supervision of Fabrizio Andreatta at the Università degli Studi di Milano.