TAGG-seminarium

Abstrakt finns enbart på engelska: 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.