Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean

Viviana del Barco, Gustavo Infanti, Exequiel Rivas +1

We present a formalization, in the theorem prover Lean, of the classification of solvable Lie algebras of dimension at most three over arbitrary fields. Lie algebras are algebraic…