Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean
Viviana del Barco, Gustavo Infanti, Exequiel Rivas, Paul Schwahn
cs.LO
May 26, 2025 · v1
TL;DR
Formalizes in Lean the classification of solvable Lie algebras of dimension at most three over arbitrary fields, extending mathlib.
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.
Problem
Lie algebras encode infinitesimal symmetries and are ubiquitous in geometry and physics, but no complete mechanized classification theorem for low-dimensional solvable Lie algebras existed in a theorem prover.
Approach
The authors formalize in Lean the classification of solvable Lie algebras of dimension at most three over arbitrary fields. The work involves explicit calculations at the vector space level and provides a use case for linear algebra and Lie theory routines in mathlib. Along the way they formalize results about Lie algebras, define the semidirect product, and add API for bases of vector spaces. Each algebra is instantiated using the commutative ring infrastructure in mathlib.
Results
The project provides a complete mechanization of the classification theorem for solvable Lie algebras up to dimension three, covering both the statement and its full formal proof, contributing to mathlib's Lie theory library.
