Milestone: 50% done

Stream: Carleson

[Floris van Doorn]

50% of the lemmas have been formalized (92/183) :tada: So the dependency graph is more than half green.

There are some caveats, and we're probably not quite at 50% of the work (especially if that includes PRing to Mathlib), but I think it's still a nice milestone.

caveats

• Lemma count is not a perfect measure of progress
• Chapter 7 will be a bit more difficult on average
• Chapter 3 is being rewritten, and will include a more general version of the main result (linearised metric Carleson), which will add some new lemmas

On the other hand, there are also a bunch of results that we have proven (e.g. the real interpolation theorem formalized by Jim Portegies) that do not correspond to explicit lemmas in the blueprint, but will still be used).

[Patrick Massot]

This is really crazy! How are you going so fast? Are you saying you formalized 75 pages of the blueprint in three months? Is it because the blueprint was really very very detailed?

[Kevin Buzzard]

This is amazing progress. I had no idea until recently that the project was going so quickly! To be honest, after having talked to Hairer about the nature of hard analysis, I was a bit scared that formalizing hard analysis might be a fair bit trickier than formalizing hard commutative algebra and that this project would be a great test to see if this were true. What I was worried about was whether analysis relied more on "principles" rather than very general theorems of the kind you find in alg geom, which apply in huge generality. In analysis the impression I got was that it was harder to formalise precise theorems which accurately summarised the complete extent of a technique.

[Patrick Massot]

I think this is true. So things in the Carlson project may be less reusable on average than in FLT.

[Sébastien Gouëzel]

I think it can be reused, but in a different sense: if you have an example of a working implementation of something using the same techniques as what you need, then you can copy-paste bits, see which lemmas are used, get an inspiration from the overall design, and so on. So it's not really useful as a black-box, but as a white-box it's super useful!

[Josha Dekker]

Perhaps we could even try to create templates of such proofs? As an added benefit, this might make it easier to distill them into theorems or tactics at a later stage?

[Yaël Dillies]

I should note that, although discrete, the analysis done in APAP is also "hard" and the same concerns and remarks (we have "principles" more than "theorems") apply, which might explain why upstreaming has stalled, cf #PR reviews > PRs from APAP

[Floris van Doorn]

The progress is indeed a lot faster than I expected. Of course, for this I have to thank all the contributors that have participated in the Carleson project so far. I want to especially mention @Jeremy Tan here, who is going above and beyond to contribute to this project, and is sending near-daily PRs.

Secondly, the blueprint is indeed very detailed. Many of the principles that are typically used on a high-level are written out carefully in this blueprint, and I need to really thank the harmonic analysis group here in Bonn for that. So far the blueprint is holding up amazingly well. We've found some minor mistakes, some typos, and a few cases where a lemma needed a slightly different proof, but all of the changes were very localized so far.

The length of the blueprint is probably a bit misleading: the original proof was ~30 pages, but that was expanded to the current page count by adding a lot more details. The proof is so detailed that even with very little experience in analysis, you can locally understand the proof of a lemma and formalize it, without knowing the full proof structure. The work by Jeremy Tan and Leo Diedering has shown this, since they knew very little about harmonic analysis before starting this project.

Finally, this project has required very few preliminaries. We didn't have to develop a theory of e.g. vector bundles first. There is a bit about doubling measures, and Jim Portegies proved the real interpolation theorem (which the blueprint actually doesn't explicitly depend on by "inlining" a proof of the special case - but we can use it in 2 places). And Mathlib is working really really well for this project. The measure theory library works well, and has e.g. (almost) all integral inequalities we need.

About the reusability: it might be true that a lot of the material is not super useful for Mathlib, and the current code quality is not (yet) Mathlib code quality. But there are definitely a bunch of reusable preliminaries that we will put into Mathlib. And we've learned design decisions. For example, a linear map $L^p(X) \to L^q(Y)$ is horrible to work with in Mathlib, and it's much nicer to just work with a transformation (X → E) → (Y → E') that has the property of behaving nicely on $L^p$ functions ( carleson#MeasureTheory.HasStrongType ).

[Filippo A. E. Nuccio]

Thanks @Floris van Doorn for the summary, very interesting.