Floris van Doorn: Progress report on the Carleson Project

Stream: Lean Together 2025

[Floris van Doorn]

Discussion thread

[Floris van Doorn]

Slides: carleson.pdf

[Floris van Doorn]

Unfortunately I don't have time to be around in the social time later tonight, but feel free to ask any questions here.

[Ruben Van de Velde]

Can you post the handout pdf as well?

[Kim Morrison]

I've only looked at the slides, as the video isn't up, so apologies if this was discussed.

Fast-forwarding to completion (:tada:!) of the project, it sounds like you are not intending to upstream the bulk of the proof to Mathlib. Long-term, does this mean that projects/developments needing Carleson's theorem as a blackbox will just be downstream of this project? Have you thought about a model for long-term maintenance of the project? If the current non-Mathlib-standard proof rotted, would its existence be a barrier to someone considering making a Mathlib version? (Because the academic credit, to the extent it existed in the first place, has already been "used up".)

(These are meant to be awkward questions --- this is one of the best examples so far of a significant project that others are very likely to want to use as a dependency!)

[Julian Berman]

(I think the video is already up as of.. 6 minutes ago: https://www.youtube.com/watch?v=w29spLdOFrY )

[Kim Morrison]

Maybe in cases like this the right answer is to upstream to Mathlib with a dispensation for a particular directory. i.e. we have Analysis/Carleson/Statement.lean and then Analysis/Carleson/Proof/{X,Y,Z}.lean, with a README.md file in the Proof directory saying "The development in this directory is intentionally not at the usual level of generality aimed for in Mathlib, because the proof of Carleson is so difficult. Contributors are welcome to refactor and generalize, and where appropriate move material out of this directory."

Obviously we'd want to be careful with such dispensations, but for foundational black boxes it could be okay.

[Michael Rothgang]

Good question! In practice, I'm more worried about the practical aspect of upstreaming (finding somebody with the time to do it)... the "dispensation" sounds like an interesting idea, to be employed with care.

[Yaël Dillies]

In an alternative world I am employed full-time upstreaming other people's projects :innocent:

[Ruben Van de Velde]

How are you doing on upstreaming your own projects? :innocent:

[Yaël Dillies]

One of them doesn't have a Mathlib folder anymore!

[Floris van Doorn]

Ruben Van de Velde said:

Can you post the handout pdf as well?

I'm not sure what you're asking for. Some printer-friendly version of the slides?

@Kim Morrison: This was not discussed, and these are good questions. I think these are also much broader questions than just for the Carleson project. I am definitely intending to keep the Carleson project compiling with the latest version of Lean for the foreseeable future. That seems like it comes at a relatively cheap cost (~30 minutes of work per month?), at least when the number of such projects is relatively small.

I can broadly see three options for the Carleson project and similar projects:
(1) It stays as a separate project, and to use it you have to add it as a dependency;
(2) It becomes part of Mathlib, violating Mathlib's usual standards on generality;
(3) We start a new centralized repository (along the lines of a Archive of Formal Proofs for Lean) that has only a few inclusion criteria[1] ensuring that the code is relatively maintainable, but no promises on the "proper generality" of these results, or partially duplicating something else.

Each of these has upsides but also significant downsides.
I'm starting to look more favorable on option (3): it will take a large amount of work to keep it updated, but maybe that is worth it compared to the current situations where many (small) projects don't get updated at all. There are costs and advantages here...

[1] Possible inclusion criteria: all/most Mathlib linters pass + doesn't compile too slowly + nothing in the root namespace + has done an effort to put parts in Mathlib + has some amount of documentation/references.

[Ruben Van de Velde]

Yeah

[Ruben Van de Velde]

Re (3) - if we set this up, we probably want to avoid a situation where trouble bumping one of the projects blocks everything else

[Kim Morrison]

I think to be honest I would be opposed to (3) (at least in the sense of not wanting to be part of the "we") unless it came with a medium term plan to pay someone to do the upgrading work. If it came with such a plan then worth exploring!

[Floris van Doorn]

I agree, (3) is conditional on having someone who has is paid (at least part-time) to do the updating.

I will keep the option in mind to request funding for something like this in upcoming grant proposals (I'm not planning anything in the short term).