Tue 18 Jan 2022 14:20 - 14:45 at Salon III - Formalization of Logic, Algebra and Geometry Chair(s): Andrei Popescu
Lie algebras are an important class of algebras which arise throughout mathematics and physics.
We report on the formalisation of Lie algebras in Lean’s Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none is assumed.
Particular attention is paid to the construction of the classical and exceptional Lie algebras. Thanks to these constructions, it is possible to state the classification theorem for finite-dimensional semisimple Lie algebras over an algebraically closed field of characteristic zero.
In addition to the focus on Lie theory, we also aim to highlight the unity of Mathlib. To this end, we include examples of achievements made possible only by leaning on several branches of the library simultaneously.
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
Tue 18 Jan
Displayed time zone: Eastern Time (US & Canada) change
13:30 - 15:10
Formalization of Logic, Algebra and GeometryCPP at Salon III
Chair(s): Andrei Popescu University of Sheffield
|Semantic cut elimination for the logic of bunched implications, formalized in CoqDistinguished Paper AwardRemote|
Dan Frumin University of GroningenPre-print Media Attached
|Undecidability, Incompleteness, and Completeness of Second-Order Logic in CoqRemote|
Mark Koch Saarland University, Dominik Kirst Saarland UniversityPre-print
|Formalising Lie algebrasRemote|
Oliver Nash Imperial College, LondonPre-print Media Attached
|A Machine-Checked Direct Proof of the Steiner-Lehmus TheoremInPerson|
Ariel Kellison Cornell UniversityPre-print