Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2505.19975 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910968735334400 |
|---|---|
| author | del Barco, Viviana Infanti, Gustavo Rivas, Exequiel Schwahn, Paul |
| author_facet | del Barco, Viviana Infanti, Gustavo Rivas, Exequiel Schwahn, Paul |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_19975 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean del Barco, Viviana Infanti, Gustavo Rivas, Exequiel Schwahn, Paul Logic in Computer Science Rings and Algebras Representation Theory 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. |
| title | Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean |
| topic | Logic in Computer Science Rings and Algebras Representation Theory |
| url | https://arxiv.org/abs/2505.19975 |