Dagur Asgeirsson, University of Alberta: Formalizing solid abelian groups
Overview
The event has passed
Date:
Starts 26 August 2026, 13:15Ends 26 August 2026, 14:15Location:
MV:L15, Chalmers tvärgata 3Language:
English
Abstract: Solid abelian groups play an important role in condensed mathematics, with applications in arithmetic geometry and $p$-adic representation theory. I will describe a Lean formalization of their theory and the additions to mathlib that made it possible.
Most of the project was a manual effort, but its completion was accelerated in recent months by coding agents. It provides a case study in how AI is changing formalization, and in why formal proof may become more important as AI systems contribute to mathematical research.
Dennis Eriksson
- Professor, Algebra and Geometry, Mathematical Sciences