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)


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.

More about the Tutorial

LftCM Colloquium

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.

More about the Colloquium

Programme Overview

Sept 4, 2023
Sept 5, 2023
Sept 6, 2023
Sept 7, 2023
Sept 8, 2023
9:00–10:00 Tutorial Tutorial Tutorial Tutorial
10:00–11:30 Colloquium
15:00–16:00 Colloquium
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: lftcm2023hhu.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.