ITP paper

Stream: general

[Rob Lewis]

In case there was any doubt: we're pleased to announce that Ellenberg and Gijswijt's solution to the cap set problem (https://arxiv.org/abs/1605.09223) is definitely correct!

The Lean code still needs a bit of cleanup. We'll make that public very soon. But in the meantime, here's a draft of our paper for ITP: https://lean-forward.github.io/e-g/e-g.pdf

We'll submit this on Sunday. Any comments or suggestions before then are more than welcome.

[Kevin Buzzard]

@Johannes Hölzl and Rob I am really pleased that you have managed to get this job out the door. Jordan asked me about its progress several times and I was scared that Johannes was going to leave Amsterdam and the project was going to peter out before it was finished.

I have said this several times before but let me try and hammer the point home again. Professional mathematicians do not really seem to care that old results like the odd order theorem have been formally verified. This is counterintuitive to me but it is absolutely what I see in practice when I talk to mathematicians up and down the UK. These results are old and people have proved far more nowadays, so they know the original results are fine and don't need formally verifying. What I am trying to do with the perfectoid project, and what this paper I think does very well, is to say "look, modern maths can be formalised nowadays, formalisers are a tool and this tool is being used to analyse recent stuff. Formalisers are becoming relevant". This paper adds more weight to my argument. Mathematicians still seem to think that formalising a paper like this is out of reach, or will take forever or something.

[Johan Commelin]

theorem theorem_12_1 ← what is that :question: :exclamation:

[Johan Commelin]

I thought those names belonged to old school pen and paper maths

[Rob Lewis]

To be fair, this paper is really a special case. Sander insisted that I tone down some of the language about how this shows "formalizing modern mathematics is within reach." This is probably the only recent Annals paper that we could have formalized with this amount of effort.

[Rob Lewis]

@Johan Commelin See the shouting note in the following paragraph. :)

[Rob Lewis]

The theorem names mirror Sander's informal blueprint. We haven't had a chance to change them yet.

[Kevin Buzzard]

So what's your next target paper? ;-) I don't think you should drop your standards -- another Annals paper?

[Sebastien Gouezel]

You could go for http://annals.math.princeton.edu/articles/14284 (Definitely hard, but not completely crazy :)

[Rob Lewis]

I have a backlog of stuff to finish and write up. We'll see if that happens before or after the next formalization paper!

[Kevin Buzzard]

You've done an Annals paper -- you could do something else. Sander is a number theorist, right? Why not formalise one of the number theory millenium problems -- the Birch and Swinnerton-Dyer conjecture would be the natural one. In broad strokes I don't see any reason why the strategy you adopted couldn't work again. Sander would be capable of taking the conjecture apart and creating a document which you could work from. For extra brownie points you could formalise the refined version. It would not surprise me if (a) the weak version had been formalised before, in some form, in a theorem prover, and (b) the strong version had not. You would end up making several conjectures, for example you would have to state the known theorem, whose proof is extremely deep, that the L-function of the curve has analytic contuation to the point s=1. But then to state the weak form of the conjecture you would just need to prove the rank of an elliptic curve is finite, which Sander and you could do I'm certain, and formalise some basic definitions in complex analysis like the order of the zero of a function. To formalise the strong version would be much more of a challenge. You would have to formalise the conjecture that the Tate-Shaverevich group of an elliptic curve is finite, which needs the absolute Galois group of Q (any news on absolute Galois groups @Chris Hughes @Kenny Lau ), group cohomology (which is not hard, you only need H^1) and the Neron-Tate height, which again would require someone who knows some number theory taking the maths definition and porting it to Lean. For the fudge factors you would need Tate's algorithm over the p-adic numbers, but this would be easy to formalise given that you have the p-adic numbers.

[Sebastien Gouezel]

We'll submit this on Sunday. Any comments or suggestions before then are more than welcome.

Couldn't you give an explicit and reasonable value for B in the main theorem (for q=3)? It would make the statement more neat, as you could put n and A and the fact that A has no arithmetic progression as assumptions instead of stuff in the middle of a chain of implications

[Sebastien Gouezel]

And you don't need n>0 in this theorem, I think.

[Rob Lewis]

We could give an explicit value. "Reasonable" isn't so clear, it isn't a pretty number. Honestly, I think it might make the statement messier, not neater.

[Rob Lewis]

Think you're right about the n>0, thanks.

[Sebastien Gouezel]

Don't give the optimal value with square roots and everything, use a larger integer. What about B = 5, say? Or is it rather B = 10^{10}?

[Rob Lewis]

Oh, fair point. B is a little less than 56.

[Patrick Massot]

@Rob Lewis, do you plan to make Sander's blueprint public? I think it would be extremely helpful, as an example of a blueprint which is detailed enough for formalization. I'm sure @Kevin Buzzard would love to see that

[Rob Lewis]

It's up to Sander. The blueprint isn't written to be made public at the moment and it would take some effort to polish.

[Patrick Massot]

I wouldn't want to see a polished version. I'd like to see a version that was good enough for formalization, but without useless work.

[Kevin Buzzard]

Patrick had a really hard time getting me to write a blueprint for the perfectoid project. I would just point to the literature and say "what's wrong with that?". And then every now and then I would run into a wall and say "oh crap I wasn't expecting that, this will be some work to sort out".

[Rob Lewis]

Sander and I discussed this today. He'll make the writeup presentable and put it online soon, hopefully before the paper deadline on Sunday.

[Rob Lewis]

Don't give the optimal value with square roots and everything, use a larger integer. What about B = 5, say? Or is it rather B = 10^{10}?

Turns out B=198 works reasonably smoothly!

[Rob Lewis]

The final draft of our paper, along with Sander's blueprint and our (still messy) Lean code, is here: https://lean-forward.github.io/e-g/

[Kevin Buzzard]

@Rob Lewis did you see Tim Gowers' question "I wonder whether the slice rank argument has also been formalized." on Jordan's twitter feed?

[Kevin Buzzard]

https://twitter.com/wtgowers/status/1111356008029474816

@JSEllenberg I wonder whether the slice rank argument has also been formalized.

- Timothy Gowers (@wtgowers)

[Rob Lewis]

Yes, I saw it. No, it hasn't. Sander added a line to the paper: "We also note that Tao [30] reformulates Ellenberg and Gijswijt’s proof in a more symmetric way, using what is now called “slice rank.” Although this is arguably a more natural way to express things, the underlying arguments are essentially the same."