Lean for the Curious Mathematician 2023
This page is for a past event. For recordings and slides, see the schedules on the Tutorial page and the Colloquium page. For similar events in the future, consult the Lean Community Events page.
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:
LftCM Tutorial
4–7 September (Mo–Th)
Düsseldorf
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.
LftCM Colloquium
7–8 September (Th–Fr)
Düsseldorf
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.
Programme Overview
| Monday Sept 4, 2023 |
Tuesday Sept 5, 2023 |
Wednesday Sept 6, 2023 |
Thursday Sept 7, 2023 |
Friday Sept 8, 2023 |
|
|---|---|---|---|---|---|
| 9:00–10:00 | Tutorial | Tutorial | Tutorial | Tutorial | |
| 10:00–11:30 | Colloquium | ||||
| 11:30–12:30 | |||||
| 14:00–15:00 | |||||
| 15:00–16:00 | Colloquium | ||||
| 16:00–17:30 | |||||
| 19:00–21:00 | Pizza | Dinner |
Organizing Committee
Local organizers:
Alexander Bentkamp (scientific programme),
Jon Eugster,
Immi Halupczok, and
Marcus Zibrowius (budget)
Scientific advisors:
Jeremy Avigad,
Johan Commelin,
Heather Macbeth, and
Patrick Massot
Secretarial support: Katja Schlingensief
Contact: lftcm2023
hhu.de
Previous Editions
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.
