Milestones

Stream: Carleson

[Floris van Doorn]

[separated this out from the new outstanding task thread]
We recently reached another (small) milestone: I finished formalizing the statements of all lemmas from the blueprint, including those of chapter 3, so the dependency graph contains no more white nodes.

Some statictics: we've now proven 143/179 lemmas & theorems, so there are 36 results remaining (20 for the main result, 16 for the reduction to the classical result). There are currently 88 (uncommented) sorry's in the repository.

The fact that there are more sorry's is explained by:

• some lemmas consist of multiple Lean statements (most extremely, Lemma 10.2.5 is separated into 21 Lean lemmas)
• there are a few partial proofs with multiple steps sorry'd
• there are a few sorry's we can remove after we finish the ENorm refactor (task 117).

[Kevin Buzzard]

Re: "I finished formalizing the statements of all the lemmas from the blueprint" -- I would argue that this is a huge and really important milestone. Can you confirm that there is no sorried data in the project at all?

[Floris van Doorn]

Yes, I just manually checked, and I'm quite confident that all sorry's are proofs.
(There might be some data defined in the middle of the proof of some individual lemmas that are currently sorry'd, of course.)

[Floris van Doorn]

And maybe I'm underselling the milestone :-)

[Kevin Buzzard]

You're definitely allowed to have "future sorried data"! Congratulations!

[Floris van Doorn]

We're reaching the endgame of the formalization: all tasks to prove both the general metric_space_carleson and the classical result classical_carleson have been claimed!