Lean for the Curious Mathematician 2023 Colloquium

Thursday 7 & Friday 8 September, Düsseldorf

This page is for a past event. For recordings and slides, see the schedules below and on the Tutorial page. Many of the recordings are also available on our YouTube channel. 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?

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.

All talks will take place in lecture hall 5K, on the main campus of Heinrich Heine University. Please make your own arrangements regarding accommodation.


Thursday, Sept 7, 2023
Lecture Hall 5K

Gihan Marasingha (Exeter)

Lean into Learning: Bridging Educational Gaps and Assessing Progress in Mathematics

This presentation delves into the transformative role of Lean in smoothing the transition from school to university mathematics, while exploring its promising but complex potential in summative assessment. Based on first-hand experiences from teaching a large cohort of first-year undergraduates and outreach work in schools, we'll discuss how Lean demystifies intricate concepts and fosters active student engagement. Additionally, we'll critically examine the use of Lean for summative assessments in a large-scale undergraduate course, identifying not only its distinct advantages but also grappling with its inherent challenges. This talk aims to provide a comprehensive, balanced view of Lean's impact and its potential to revolutionise mathematics education and assessment.

Video (Password: LftCM2023)

Coffee break

Rémy Degenne (Lille)

Probability in the Lean mathematical library

The Lean mathematical library, mathlib, is a growing collection of mathematical results from algebra, analysis, topology, measure theory, etc., put together in the same formal library in a way that makes them compatible with each other. Building on all those fields, we recently started the development of probability theory. I will present an overview of the current probability results in mathlib and focus in particular on work done in collaboration with Kexing Ying on stochastic processes, martingales and Doob's convergence theorems. I will also discuss future progress and identify important results which could now be formalized by interested contributors.

Video (Password: LftCM2023)


Sebastian Ullrich (Lean FRO)

Special Announcement: The Lean Focused Research Organization

Video (Password: LftCM2023)

19:00–21:00Dinner at Wilma Wunder
(registered participants only)

Friday, Sept 8, 2023
Lecture Hall 5K

Cezary Kaliszyk (Innsbruck)

Not only Lean: Features of Other Proof Assistants

In this talk, I will discuss the distinguishing features of the various proof assistants. I will start with a short introduction to the history of interactive theorem proving. I will continue with the discussion of proof assistant foundations, set theory and HOL. Next I will discuss the strengths of the various approaches, including proof languages, automation, and formal proof readability.

Video (Password: LftCM2023)

Coffee break

Floris van Doorn (Paris-Saclay)

The Independence of the Continuum Hypothesis in Lean

In 2019 I formalized the independence of the continuum hypothesis in Lean together with Jesse Han. The continuum hypothesis states that there is no cardinality between the cardinalities of ℕ and ℝ, and was famously proven independent of ZFC by Paul Cohen in 1963. We used Boolean-valued models to give forcing arguments for both the consistency of CH and the unprovability of CH. Boolean-valued models are models where relations (like membership) take values in a chosen Boolean algebra.

In this talk I will look back at the project and explain the proof and the design decisions we used in the project. Due to the work of Aaron Anderson the basic model theory used in the project was improved and incorporated in mathlib, and I will also discuss this.

Slides · Partial video (approx. 40 minutes) (Password: LftCM2023) · Flypitch project


Oliver Nash (Imperial)

On a formalization of Gromov's h-principle and Smale's sphere eversion theorem in Lean

Since different branches of mathematics present different challenges to the formal mathematician, it is important to formalise as varied a collection of results as possible. The challenges presented by algebra or combinatorics certainly differ from those presented by differential topology, where an informal proof might just be a picture. Massot thus proposed the challenge to formalise a deep result in differential topology (Gromov's h-principle for first-order open, ample differential relations) together with a famous counter-intuitive corollary: Smale's sphere eversion theorem. We will discuss the successful completion of this challenge by van Doorn, Massot, and the speaker. No knowledge of differential topology will be assumed, and the emphasis will be on general lessons for today's formal mathematicians.

Slides · Video (Password: LftCM2023) · Sphere eversion project


Kaiyu Yang (Caltech, remote)

Theorem Proving via Machine Learning

Machine learning, especially large language models (LLMs), has shown promise in mathematical reasoning. This talk provides a comprehensive introduction to leveraging machine learning for theorem proving in proof assistants, such as by automatically suggesting useful tactics or premises. After a broad overview of existing work in this domain, I will focus on LeanDojo: an open-source suite of tools, datasets, and models for developing LLM-based theorem provers. Finally, I will discuss ongoing projects and future steps for integrating machine learning tools into the workflow of Lean users.

Slides · Video (Password: LftCM2023) · LeanDojo