News
- Talk in the INdAM seminar seriesI will give the talk “Can We Really Trust a Lean Proof? What We Gain from Human- and AI-Written Proofs” at the INdAM seminar series Lean, Formalized Mathematics and AI-Assisted Discovery on 14 December 2026 at 14:30 CET. Watch on YouTube.
- Demailly Prize ceremony for mathlib
- Talk at the Séminaire de géométrieI will speak at the Séminaire de géométrie on 21 September 2026 (slides).
- Demailly prizemathlib was awarded the 2026 Demailly Prize!
- Kummer's criterion formalized in LeanTogether with Chris Birkbeck, we formalized (using LLMs) Kummer’s criterion for regularity. See the repository.
- Talk at Colloquia PatavinaI am giving a talk Around Formalization: Why and How to Explain Mathematics to a Computer at the Colloquia Patavina (slides).
- New preprint out!Synthetic Differential Geometry in Lean, with Gabriella Clemente. To appear in the Annals of Formalized Mathematics.
- Lean for the Curious Mathematician 2026The workshop will offer an opportunity to gain hands-on experience with Lean under the guidance of expert tutors.