Formalizing structures in an algebraic hierarchy

Axiomatically characterized abstract structures have been central to mathematics since the early twentieth century. The ability of Lean and its mathematical library, Mathlib, to manage a complex network of such structures has been essential to their acceptance by the mathematical community. In this talk, I will discuss some of the challenges that structural reasoning brings and how they are addressed in Lean and Mathlib. The talk is accessible to a general math audience.