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.