News
- 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!
- Lean for the Curious Mathematician 2026The workshop will offer an opportunity to gain hands-on experience with Lean under the guidance of expert tutors.