We extend the mathematical library of the Lean interactive theorem prover with basic definitions and results about abelian categories. Within this theory, we formalize the notion of pseudoelement, which generalizes the notion of element in an abelian group to a general arrow-theoretic setting and gives access to the proof technique of diagram chasing. Using the metaprogramming framework of the Lean theorem prover, we develop tactics that semiautomatically synthesize proofs of statements about commutative diagrams in abelian categories using pseudoelements. Using this, we give the first formally verified proof of the snake lemma, an important tool in homological algebra with ample applications in pure mathematics and beyond.
Keywords
Lean, formalization
Publications
Advisors
Students
