The Carleson project: a collaborative formalization

Mathematical formalization consists of digitizing mathematical definitions and results using a `proof assistant', a computer program capable of checking whether a proposition can be deduced from a set of inference rules and a collection of basic axioms. In recent years, the community of mathematicians working on formalization has grown rapidly and has reached milestones that demonstrate the ability to formalize results at the frontier of knowledge. Proof assistants have applications to mathematics research, teaching, and communication.

In this talk I will describe a collaborative project whose goal was to formalize a result from modern harmonic analysis. The talk will focus on the organization of the collaboration and the lessons we learned during the formalization process.

A well-known result in Fourier analysis establishes that the partial Fourier sums of a smooth periodic function $f$ converge uniformly to $f$, but the situation is a lot more subtle in more general settings (for instance, when $f$ is a continuous function). However, in 1966 Carleson proved that they do converge at almost all points for $L^2$ periodic functions on the real line. Carleson’s proof is famously hard to read, and there are no known easy proofs of this theorem. 

We formalized in Lean a generalization of Carleson’s theorem in the setting of doubling metric measure spaces (proven by the Bonn harmonic analysis group in 2023), and Carleson's original result as a corollary.