CIRCA seminar August 1st
Peiran will give a seminar at 1pm on Thursday 1st August, in Theatre C of the Mathematical Insitute
Title: Turning the classification of groups of order pq into Lean code
Abstract: Lean is a programming language designed for interactive theorem proving – formalising mathematical definitions, statements, and proofs as computer code. Owing to a decade of community efforts, the language’s mathematical library “Mathlib” has seen very fast growth and currently contains more than 1.5 million lines of code. However, the library still lacks many basic results in group theory. In joint work by me and Scott Harper, we formalised a classification of groups of order pq, where p and q are two arbitrary prime numbers. I will speak about our design choices, surprises we encountered during the project, and what we learned along the way.