The Carleson Project: Collaboration using Formalization

In 1966 Lennart Carleson published a proof of an important theorem in harmonic analysis, that states that the Fourier series converges pointwise to the original function under weak conditions. This result has a notoriously difficult proof, and while the result has been generalized, every found proof is full of intricate details. In my talk I will describe an ongoing formalization project that verifies all the details of a generalized Carleson theorem in Lean. I will in particular reflect on the collaborative nature of this formalization.