A new #Lean4 formalization project has been launched , to prove Carleson's famous theorem on pointwise convergence of Fourier series (as well as some more modern generalizations of that theorem). The main web page for the project (containing the blueprint and github repository for the Lean files, etc.) is at https://florisvandoorn.com/carleson/ , and the Zulip channel to coordinate the project is at https://leanprover.zulipchat.com/#narrow/stream/442935-Carleson
@tao
The project page says that it formalizes a recent proof by Thiele et al that was not published yet. Is the proof similar enough to existing ones, or is the structure of it clear enough from the blueprint, so that people from the field can tell that the proof is correct?
@Pashhur The blueprint does contain a lot of material (such as classical Calderon-Zygmund theory) that is quite standard in this area, and Thiele is one of the leading world experts in the subject and has not to my knowledge published anything with major errors in it. Furthermore, the blueprint is already rather more detailed than a traditional math paper, even if it has not yet been properly formalized. So I think there is a reasonable a priori probability to expect that the arguments are largely correct. That said, the formalization effort, despite being only a day or two old, has already uncovered some minor issues in the blueprint (a (k) should have been a (k+1) in one of the lemmas, for instance): https://leanprover.zulipchat.com/#narrow/stream/442935-Carleson/topic/Outstanding.20Tasks.2C.20V1
@tao Thanks Terry and everyone on the Zulip channel for the support of this project. We are working on fixing the blueprint errors that were pointed out in the channel. So far they are small in the sense they require only localized corrections. They remind us why we are doing the computer verification at the first place.
Introducing Carleson type operators on doubling metric measure spaces was originally a non-Lean research project. The new level of generality would have been very surprising 15 years ago, but now is a bit less so after related research in recent years. The abstraction makes the proof particularly suited for computer verification, so we turned it into a Lean project that will include a computer verification of the classical Carleson theorem.