You are here: Seminars > 2024 > September 25th
University of St Andrews
Time: 16:00-17:00 (GMT+8), Wednesday September 25th, 2024
Location: Zoom
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 give a quick introduction to Lean, explain how we structured the code in the project, and share what we learned along the way.
Host: 黄弘毅 Hong Yi Huang