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 weakconditions. This result has a notoriously difficult proof,and while the result has been generalized over the years, every found proof is full of intricate details.In my talk I will describe an ongoing formalization project that verifies all the details of ageneralized Carleson theorem in Lean. I will in particular reflect on the collaborative natureof this formalization.
