Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean
Exequiel Rivas
Tallinn University of Technology
Abstract:
In this talk, we will discuss the experience of formalizing a classification
theorem for solvable Lie algebras of dimension at most three in the Lean
theorem prover. We will briefly introduce the mathematics required to
understand the statement (no prior background in Lie theory will be assumed)
and explain the motivation behind formalizing the result. We will outline the
process of formalizing these results using mathlib (the unified mathematical
library for Lean), and the challenges encountered along the way. Finally, we
will conclude with an update on the current status of the project and what we
expect to continue working on in the future.