Autor(es)

del Barco, Viviana ; Infant, Gustavo ; Rivas, Exequiel ; Schwahn, Paul

• Tipo de documento: Artigo Científico
• Fonte: INTELLIGENT COMPUTER MATHEMATICS, CICM 2025; v. 16136, p. 23-pg., 2026-01-01.

Resumo

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. (AU)

• Processo FAPESP: 23/15089-9 - Aspectos da geometria conforme e Riemanniana em grupos de Lie e seus quocientes compactos.
• Beneficiário: Viviana Jorgelina Del Barco
• Modalidade de apoio: Auxílio à Pesquisa - Regular
• Processo FAPESP: 24/08127-4 - Laplacianos em espaços homogêneos
• Beneficiário: Paul Valentin Schwahn
• Modalidade de apoio: Bolsas no Brasil - Pós-Doutorado