This institute colloquium featured two talks on formalising mathematics in the Lean proof assistant.
Speakers: María Inés Frutos Fernández and Michael B. Rothgang (University of Bonn)
- Michael Rothgang: Formalising differential geometry in Lean
- María Inés de Frutos Fernández: Number Theory in the Lean Theorem Prover