Professional Summary
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.
News
Talk at Colloquia Patavina
I am giving a talk Around Formalization: Why and How to Explain Mathematics to a Computer at the Colloquia Patavina.
New preprint out!
Synthetic Differential Geometry in Lean, with Gabriella Clemente.
Register for Lean for the Curious Mathematician 2026!
The workshop will offer an opportunity to gain hands-on experience with Lean under the guidance of expert tutors.