Lean for the Curious Mathematician 2023 Tutorial

4–7 September (Mo–Th), Düsseldorf

This page is for a past event. For recordings and slides, see the schedules below and on the Colloquium page. Many of the recordings are also available on our YouTube channel. The exercises are available from a public GitHub repository. 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 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.

Starting from the basics (how to install and use Lean, essential mechanisms for formalizing mathematics, navigating the proof library mathlib, …), the lectures will build up towards more advanced topics that illustrate how formalization works in different areas of mathematics. The specific areas covered will depend largely on the participants' interests (e.g. real and complex analysis, number theory, topology, combinatorics, category theory, …).