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).