Seminario Teoría de Grupos
An introduction to formalizing mathematics in Lean
Ponente: Hang Lu Su ()Fecha: jueves 21 de mayo de 2026 - 11:30Lugar: Aula Gris 2, ICMAT
Resumen:
Recent advances in AI-assisted theorem proving have made Lean 4 increasingly relevant to working mathematicians. Lean serves both as a proof assistant for human formalization and as a verification environment for automated systems. Its relevance to research-level mathematics was demonstrated by the Liquid Tensor Experiment, proposed by Peter Scholze and completed in 2022. More recent AI-assisted examples include the recent submission of P. Monticone’s Kourovka Notebook Problem 21.24, 20.125 and 20.150 solution notes from March 2026, which report that the solutions were autonomously discovered and formally verified in Lean 4 by Aristotle, a formal reasoning agent developed by Harmonic. In this seminar, I will introduce the basic ideas of formalizing mathematics in Lean, give a short demo, and discuss my recent progress formalizing finitely presented groups for mathlib4, the largest library of formalized mathematics written in Lean.
