这是群论和图论方向的线上系列报告，我们希望能够促进国内外青年学者（博士生为主）在群论和图论研究上的交流。报告主题分布在（但不限于）以下研究方向：
This is a platform for young group theorists and graph theorists (mostly PhD students) to talk about their research and related topics online. The topic can be anything related to group theory and graph theory, including but not limited to the following.
一般地，系列报告定期于北京时间每周三下午16:00-17:00进行。
Our usual time is Wednesday 16:00-17:00 (GMT+8).
Title: Turning the classification of groups of order \(pq\) into Lean code
Speaker: 吴培然 Peiran Wu (University of St Andrews)
Time: 16:00-17:00 (GMT+8), Wednesday September 25th
Location: Zoom: 616 601 4311 (passcode: gts2024)
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.
The seminar is currently based at the Southern University of Science and Technology (SUSTech, 南方科技大学).