Kummer's criterion formalized in Lean — Together with Chris Birkbeck, we formalized (using LLMs) Kummer’s criterion for regularity. See the repository.
Talk at Colloquia Patavina — I am giving a talk Around Formalization: Why and How to Explain Mathematics to a Computer at the Colloquia Patavina (slides).
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.