A recent proof about Ramsey numbers

Stream: maths

[Bhavik Mehta]

I'd like to announce that I've finished formalising the main result of this paper: https://arxiv.org/abs/2303.09521, which gives the first exponential improvement to the upper bound on diagonal Ramsey numbers. This improves on a 2009 paper in the Annals, making it the second formalised proof I've done which beats a 21st century Annals paper! Kevin has very kindly allowed me to have a guest post on his blog, in which I give more mathematical details: https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/.

[Patrick Massot]

Is any reason why you posted this on Kevin's personal blog instead of the Lean community blog?

[Patrick Massot]

I hope you realize people all over the world will talk about how Kevin formalized yet another Annals paper.

[Bhavik Mehta]

Patrick Massot said:

Is any reason why you posted this on Kevin's personal blog instead of the Lean community blog?

Yes, because it's in Lean 3 and not Lean 4.

[Patrick Massot]

I don't understand how that is relevant. But it's your project, you are free to do whatever you want. I simply brings back bad memories that are precisely the reason why we created the community blog.

[Antoine Chambert-Loir]

@Bhavik Mehta , could you detail what you mean by Footnote 5 : “It should – in principle – be possible to port the formalisation to Lean 4, but at the moment it seems more difficult than one might hope.”

[Bhavik Mehta]

Sure! In brief, it's because so far in the porting process I've hit regressions very often (about 1 every 30 lines). Some have been solved since I found them, but the relative rates of finding and fixing are such that I don't think it's particularly easy. There are some regressions I can work around (like the equation compiler being weaker, and the code generator being incomplete), but others where fixing the proof would require quite a bit of effort if the fix takes a while to land in a release of Lean. There's also just the fact that when I do hit a regression far into the proof, it's a non-trivial amount of work to identify what the actual problem is, in order to report it as a regression! I was actually originally much more pessimistic in this Footnote, because of the decide and simp regressions which I'd found very early on in this proof, but these have since been fixed.

[Patrick Massot]

Documenting those issues is a lot of work but it is very worthwhile. Especially since you have an uncommon use of Lean, you are likely to find issues that nobody else finds. So your porting work is very valuable to the community. Of course Lean 4 is globally much better than Lean 3, but it doesn't mean it better in every direction. A lot work remain. And we will never reach a perfect improvement in every direction. Some proofs worked in Lean 3 using "features" that were massive performance bottlenecks and have been removed from Lean 4. Those require real porting work independent of bug fixes.

[Bhavik Mehta]

Patrick Massot said:

Documenting those issues is a lot of work but it is very worthwhile. Especially since you have an uncommon use of Lean, you are likely to find issues that nobody else finds. So your porting work is very valuable to the community. Of course Lean 4 is globally much better than Lean 3, but it doesn't mean it better in every direction. A lot work remain. And we will never reach a perfect improvement in every direction. Some proofs worked in Lean 3 using "features" that were massive performance bottlenecks and have been removed from Lean 4. Those require real porting work independent of bug fixes.

Yes, I couldn't agree more. The intended meaning of the footnote was to indicate that I would like to document these issues, even though I know it will be tough.

[Bhavik Mehta]

In fact let me go further - what's the best way for me to log and share the issues I find, to distribute the work of minimising / isolating why something works in Lean 3 and doesn't in Lean 4, and hence figure out whether it's a regression or not?

[Patrick Massot]

The main game here is minimization. First go from an issue in your project to an issue in a file depending only on Mathlib. For this first step I'm afraid you will have a very hard time finding help. Then you can post a message in the mathlib4 stream on Zulip asking whether anyone recognizes this as a known issue. If it isn't recognize then a new minimization step tries to get rid of the Mathlib dependency. Here you can hope to get some help. Sometimes you can't because the issue is in Mathlib and we need to work on it. Otherwise we reach a Mathlib-free example and you can open a Lean 4 issue. Then you can try to convince Scott to label this issue as high priority for Mathlib.

[Bhavik Mehta]

Ah okay, the first step is exactly what I'm worried about. But no worries, I've done it a couple of times already, I can keep going.

[Patrick Massot]

I know. I have exactly this problem with the sphere eversion project. That's where all my simp issues report come from.

[Mauricio Collares]

Would it make sense to have a thread/stream for requesting minimization help?

[Kevin Buzzard]

You mean as a stop gap until someone figures out how to do this programatically?

[Mauricio Collares]

We're all a stop gap until someone figures out how to do this programatically, so yes :)

[Geoffrey Irving]

Should we have a zulip? tactic?

[Geoffrey Irving]

It would construct the MWE automatically using Anne’s iterated minimization program. :)

[Mauricio Collares]

But seriously, a tactic to minimize it automatically would be wonderful

[Kevin Buzzard]

@Anne Baanen has been working on one (although speaking as someone who's examining their thesis next month I can confirm that they've also been working hard on their thesis)