What is... mathematical formalization?Graduate Colloquium

by María Inés de Frutos Fernández (MI)

Wednesday Nov 26, 2025, 3:15 PM → 4:45 PM Europe/Berlin

Endenicher Allee 60, Nebengebäude/N0-003 - Seminarraum (Mathezentrum)

Abstract:

Mathematical formalization is the process of digitizing mathematical definitions and results using a "proof assistant" (e.g. Lean), that is, a computer program capable of checking logical statements against a set of inference rules and some basic axioms. In recent years, the community of mathematicians working on formalization has grown rapidly and has reached milestones that demonstrate the ability to formalize results at the frontier of knowledge. In this talk, I will give an introduction to formalization, survey recent formalization projects, and discuss applications to mathematical research, teaching, and communication. No previous knowledge in this area will be assumed.

 

Website of the Hausdorff Colloquium