Oliver Nash (Imperial College London), Toward the classification of semisimple Lie algebras in Lean
Abstract: I will discuss the theory of Lie algebras as formalised in Lean's mathematics library, Mathlib. As often in formal mathematics, it has proved worthwhile to develop the theory at a level of generality beyond what is found in standard foundational texts. I will share some examples of the impact this has had on Mathlib. I will also outline approximately how much work remains until we can add a complete formal proof of the Cartan-Killing classification to the library.
Coffee break
Alain Chavarri Villarello (Vrije Universiteit Amsterdam), Formally certifying rings of integers in Lean
Abstract: The ring of integers of a number field K is the subring consisting of elements in K that are zeros of monic polynomials with integer coefficients. It is a central object in algebraic number theory and its explicit determination is relevant for numerous applications. Multiple algorithms exist to compute this ring, including the so-called Round 2 algorithm. In this talk, we will look into the formalization in the Lean theorem prover of the theoretical foundations for this algorithm. This includes the Pohst-Zassenhaus theorem and Dedekind's criterion, which, as we will see, also hold in a more general setting. We will then discuss a formal certificate for the ring of integers based on these results, which works locally prime-by-prime and only requires the verification of simple equalities.