Collaboration using formalization in mathematicsLecture

by Floris van Doorn (MI Bonn)

Thursday May 7, 2026, 9:00 AM → 10:00 AM Europe/Berlin

Endenicher Allee 60 / Lipschitzsaal (Mathezentrum)

Formalization of mathematics is a rapidly growing field that has seen exciting results in recent years, such as the formalization of the main theorem in condensed mathematics, Gromov's h-principle and Carleson's theorem. These results are formalized in Lean, building on its mathematical library Mathlib. These projects are often a collaboration between many people, more than is usual for a typical mathematical paper.

In this talk I will give an overview of Lean and its mathematical library Mathlib, and focus on the Carleson project that I led last year. In this project we formalized a generalization of Carleson's 1966 theorem in harmonic analysis about the pointwise convergence of Fourier series. This result has a notoriously difficult proof, which is fully verified in Lean. The formalization was a large collaborative project with 17 main contributors.