Project Finish

Stream: Carleson

[Floris van Doorn]

Less than 13 months after launching this formalization project, we have finished the original goal of formalizing both carleson#classical_carleson and carleson#metric_carleson. The formalization of these results is now sorry-free.

Thanks to the following people for their major contributions to this project: María Inés de Frutos Fernández, Leo Diedering, Sébastien Gouëzel, Evgenia Karunus, Edward van de Meent, Pietro Monticone, Jasper Mulder-Sohn, Jim Portegies, Joris Roos, Michael Rothgang, James Sundstrom and Jeremy Tan. I will shortly update the blueprint to add their names as coauthor to the blueprint.

Thanks to the following people for additional contributions: Michel Alexis, Bolton Bailey, Julian Berman, Joachim Breitner, Martin Dvořák, Georges Gonthier, Aaron Hill, Austin Letson, Bhavik Mehta, Eric Paul, Clara Torres, Dennis Tsar, Andrew Yang and Ruben van de Velde.

Thanks to Lars Becker, Asgar Jamneshan, Rajula Srivastava and Christoph Thiele for writing the blueprint, and an additional thanks to Lars for answering all the mathematical questions that came up during the formalization!

[Ruben Van de Velde]

Looking back at the project, would you say the formalization brought to light relevant holes in the original proof?

[Floris van Doorn]

The original pre-blueprint proof (which was ~30 pages) had no (major) gaps, and most gaps were introduced when writing the argument in a much more detailed fashion when writing the blueprint.
In the details, there were various places where the argument was slightly wrong and had to be modified a bit, but most such mistakes were confined to the proof of a single lemma. There were a few mistakes in the computation of the constants, but besides that, there were only a handful of times that we had to change the statement of one or more lemmas. And only 1-2 of these mistakes have actually affected the short (not yet public) mathematical proof.

So I don't think the formalization really gave a new mathematical insight into any holes in the proof.

[Kevin Buzzard]

It gave confidence though!