Floris van Doorn - Lessons from the Carleson project

Stream: Lean Together 2026

[Rémy Degenne]

Discussion topic for the talk.

[Floris van Doorn]

Slides

[Rémy Degenne]

Are there intermediate results that you proved only for finite objects, but for which the full version would be of interest to Mathlib? Or was that restriction to finite things only done for steps that are really specific to the Carleson proof?

[Floris van Doorn]

In my talk I mentioned the Hardy-Littlewood maximal function which we definitely want in Mathlib, and where our non-standard version is a "finite" version of it.

The argument with cubes and tiles is one that is made more frequently in harmonic analysis. They are sometimes called (Christ’s) dyadic cubes, and they are actually mentioned on Wikipedia.
Such a structure would probably be useful for Mathlib at some point, but even if we did a non-finite version of the argument, I think I would still write down only what is needed for this proof, which might need to be adapted/generalized to support most/all other settings where they are used.

[Rémy Degenne]

Ok, so the choice of going for finite means that there is more work to be done if we want to port those parts to Mathlib. I'm curious about the "finite" choice in general because I can see very easily what can be made worse for formalization by going to finite objects (and I was surprised that you chose that path).
You mentioned that a measurability proof was made easier. How much easier? Are we missing tools for the general proof, or does it just need a few more steps to reduce to a countable sup before becoming easy?

[Antoine Chambert-Loir]

Rémy Degenne said:

I can see very easily what can be made worse for formalization by going to finite objects

Can you please elaborate?

[Rémy Degenne]

Caveat: I did not follow the Carleson project and did not look closely at the code. I'm reacting from the content of the talk and might imagine the wrong kind of finite object manipulations.

I'm imagining difficulties (purely Lean difficulties, not mathematical) similar to what you can encounter if you have elements of Fin n and in parts of the arguments there is also Fin m for n < m. Suddenly you have functions defined on one of those that can't take an argument from the other one without having to provide proofs.
I see for example that in the project there are grids with a parameter S : Nat which involve things in Icc (-S : ℤ) S. If you ever consider grids with two different S somewhere that kind of issues might appear. But perhaps it's not the case in this proof.

[Floris van Doorn]

For the maximal function, we currently have only proven the measurability when we use a countable family of balls: https://github.com/fpvandoorn/carleson/blob/ddf5d418922c1dee5ca2735dfb4e2a5f31a99018/Carleson/ToMathlib/HardyLittlewood.lean#L435
I don't think the prove of its measurability is particularly hard for the standard function, but it would require a different proof.

The grids are indexed by the integers, with the assumption that all cubes lie in Icc (-S : ℤ) S. S is fixed throughout the whole proof (except maybe in a single limiting lemma). I don't think there were any problems from annoying embeddings similar to Fin n -> Fin m because of this choice.

I agree that these choices were suboptimal. They were made before the formalization started at a time when Christoph knew the math, but didn't have experience about what was hard or easy in Lean, and I didn't know the math yet. During the formalization, I also didn't know whether using a nonstandard maximal function was necessary for the proof or not.

[Snir Broshi]

Can you explain why you don't plan to upstream Carlson itself to mathlib?

[Michael Rothgang]

My understanding is that this is a combination of several factors:
(1) reusability: most prerequisites (e.g. the Hardy-Littlewood maximal function, the real interpolation theorem, more lemmas about integrals, ...) are clearly reusable elsewhere, and therefore obviously belong into mathlib. It's less clear if Carleson's theorem is of the same kind (and even so for the doubling metric measure spaces generalisation). It's not a pure endpoint theorem, but the motivation is weaker.
(2) practical considerations: who puts in the work? I think nobody would mind if you did, but there is a lot to do. The ~30 000 lines not in the ToMathlib directory are often very far from mathlib level code. Improving them would be a very large effort.

[Kevin Buzzard]

Is the following view of the future something which has a reasonable possibility of happening: in 5 years' time someone proves an important new theorem which needs Carleson as input, someone suggests formalizing it in Lean, all of the prerequisites made it to mathlib, but the main argument is still lying rotting in the Carleson repo on v4.35 and it's completely hopeless to port it to Lean v4.87 which is where mathlib is?

My understanding is that Gonthier still spends some of his time bumping the odd order proof so that it runs on today's Rocq (I heard this a few years ago so it might be a bit out of date but definitely the odd order proof compiled on a version of Coq which was released many years after the formalization was completed).

[Vlad Tsyrklevich]

(Odd order continues to be updated: https://github.com/math-comp/odd-order/releases but it doesn't look like Gonthier himself has committed recently. I believe the Rocq project maintainers PR updates to major projects if they make breaking changes, though others may also be involved in long-term maintenance.)

[Kevin Buzzard]

So somehow odd order is "part of the ecosystem". Can we make Carleson part of the lean ecosystem? I guess one issue is that lean/mathlib are not too worried about backwards compatibility for now, although my understanding of Leo's comments about this in his talk were that perhaps in a year or so lean will be much more stable.

[Patrick Massot]

Maybe the Mathlib Initiative could be interested in investing some money to make sure such projects do not rot.

[Michael Rothgang]

I'm not worried about Carleson rotting. Like sphere-eversion (which to me has a reasonable chance of getting fully into mathlib... provided enough work is invested!), I can imagine a volunteer bumping the project regularly. The amount of work required is not too large right now.

[Michael Rothgang]

That said, tooling to automate (more) of the bump would be most welcome! (And AI could actually help here: if a proof breaks that's not mathlib-level at all, just have AI re-generate a proof. Assuming we can have both ChatGPT and our planet.)

[Bas Spitters]

@Kevin Buzzard I'm hoping/ predicting that upgrading to newer versions can be automated. If not now already, likely with the progress in the coming years.

For reference, our https://github.com/rocq-community/math-classes library was written 15 years ago and still compiles with the latest version.
https://github.com/rocq-community/corn is even older.
Maintenance is shared by the Rocq community. https://github.com/rocq-community/manifesto
Maybe something similar would be useful for Lean too.