Talks

• 7–11 September 2026 — Introduction.
  Lean for the Curious Mathematician (LFTCM2026), Cortona, Italy.
• 7–11 September 2026 — Autoformalization: Formalized Mathematics in the Age of AI.
  Lean for the Curious Mathematician (LFTCM2026), Cortona, Italy.
• 23 July 2026 — An Introduction to Formalization of Mathematics: Why and How to Explain Research-Level Mathematics to a Computer.
  Cyberpunk Mathematics 2026, Westlake University, Hangzhou, China.
• 5 May 2026 — Around Formalization: Why and How to Explain Mathematics to a Computer.
  Colloquia Patavina for Students, University of Padova, Italy.