Lean for the Curious Mathematician 2023 Colloquium

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)

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)

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)

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