Lean for the Curious Mathematician 2023
Are you curious what the excitement around the proof assistant Lean is all about? Are you intrigued by recent successes in the formalization of deep mathematical theorems, and would like to understand more concretely what this formalization entails? Do you find yourself wondering how far your favorite area of mathematics is still away from being formalized, and what lies ahead?
Then Lean for the Curious Mathematician is for you! The 2023 edition will comprise two consecutive but independent events: an intensive four-day tutorial, and a shorter colloquium for the impatient, both hosted at Heinrich Heine University Düsseldorf:
4–7 September (Mo–Th)
The Tutorial will offer an opportunity to gain hands-on experience with Lean under the guidance of expert tutors. A series of lectures will systematically introduce the software and the associated mathematical library, with plenty of time left in between for problem-solving and first small projects.
7–8 September (Th–Fr)
The Colloquium will showcase recent large-scale formalization projects and teaching endeavours with Lean. It will give an impression of current developments in computer-assisted theorem proving, including recent advances deploying artificial intelligence, and invite to reflect on the future role of these technologies in mathematics.
Alexander Bentkamp (scientific programme), Jon Eugster, Immi Halupczok, and Marcus Zibrowius (budget)
Jeremy Avigad, Johan Commelin, Heather Macbeth, and Patrick Massot
Secretarial support: Katja Schlingensief
The first edition LftCM 2020 was an online event. The second edition LftCM 2022 took place in Providence, USA. Videos recordings of the previous editions are available here and here.