30. Mar 2026

Lean: Collaboration using Formalization

Datum: 30. March 2026 | 11:30 – 12:30
Sprecher: Floris van Doorn, University Bonn
Veranstaltungsort: Raiffeisen Lecture Hall
Sprache: Englisch

Lean is a proof assistant which has a large mathematical library containing results from most areas of mathematics. It contains a good foundation to verify current research problems in various areas of mathematics, and enables new collaborative projects.

In this talk I will give an overview of Lean and its mathematical library Mathlib, and describe some of the exciting formalization projects in this area. In particular, I will describe a recently finished project formalizing a generalization of Carleson's 1966 theorem in harmonic analysis, about the pointwise convergence of Fourier series. This is a major result in harmonic analysis with a difficult proof, and this result has been fully verified in Lean. The formalization was a large collaborative project with 17 main contributors.