Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean
Viviana del Barco, Gustavo Infanti, Exequiel Rivas, Paul Schwahn
TL;DR
The paper addresses the problem of fully formalizing the classification of solvable Lie algebras of dimension $≤3$ over arbitrary fields within Lean. It builds explicit Lie algebra instances on low-dimensional vector spaces, proves isomorphisms to a set of representatives, and uses invariants such as commutator dimension and center containment to show non-isomorphism among cases, aided by a semidirect product framework and almost abelian structure. The work delivers a complete, machine-checked classification and introduces new linear algebra and Lie algebra lemmas plus an API for semidirect products, laying groundwork for higher-dimensional extensions and broader formalized Lie theory in mathlib. This formalization demonstrates the viability and value of rigorous, machine-checked classification results in Lean, enhancing reproducibility and providing reusable tools for future formalizations in geometry and algebra.
Abstract
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 objects which encode infinitesimal symmetries, and as such ubiquitous in geometry and physics. Our work involves explicit calculations on the level of the underlying vector spaces and provides a use case for the linear algebra and Lie theory routines in Lean's mathematical library mathlib. Along the way we formalize results about Lie algebras, define the semidirect product within this setting and add API for bases of vector spaces. In a wider context, this project aims to provide a complete mechanization of a classification theorem, covering both the statement and its full formal proof, and contribute to the development and broader adoption of such results in formalized mathematics.