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

TL;DR

This paper formalizes the classification of low-dimensional solvable Lie algebras in Lean, providing a complete mechanization of the theorem and its proof, and enhancing the library's capabilities for Lie theory and linear algebra.

Contribution

It introduces a formal proof of the classification theorem for solvable Lie algebras of dimension up to three in Lean, including definitions, calculations, and API enhancements.

Findings

Successful formalization of the classification theorem in Lean

Development of Lie algebra and vector space APIs in mathlib

Demonstration of the utility of Lean for algebraic classification

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.