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 13 main contributors.