Millenium Problems

Stream: maths

[Stepan Nesterov]

Which of the Clay Institute Millenium Problems we can currently state in Lean?
For those we can't, what are some major ingridients missing?

[Kevin Buzzard]

All but Yang-Mills can be stated in theory. The reason your question is harder to answer than it looks is that things like the Poincare conjecture can be stated in several different ways, and sometimes it is a deep theorem that these ways coincide.

[Kevin Buzzard]

Here is another issue. For the Riemann hypothesis one could certainly prove that $\sum_{n\geq1}n^{-s}$ converges for Re(s)>1. One could just knock off easily the assertion "there is a meromorphic function on the whole complex plane which agrees with this and its only zeros in $0<Re(s)<1$ are with $Re(s)=1/2$" -- but does that count, or am I supposed to also extend the function?

[Kevin Buzzard]

For BSD, one could probably struggle to define the L-function of an equation y^2=cubic in x with rational coefficients three distinct roots but it would be doable, and one could probably even prove without too much trouble that it extends to Re(s)>2. One could also define the group structure. OK now what? Is the conjecture "the group is finitely-generated, the L-function has analytic continuation, and the order of vanishing at 1 is equal to the rank of the group"? When I learnt BSD in the early 90s the conjecture looked like that. Then Taylor--Wiles happened and by 2000 we could prove that the L-function did have analytic continuation, but this is thousands of pages of algebraic geometry, number theory and functional analysis which I would be overjoyed to see formalised in my lifetime. Does stating the conjecture involve formalising those thousands of pages, which are assumed in the statement as it is on the Clay website?

[Stepan Nesterov]

Let's extend the scope of the question slightly to say that if there is a reformulation that is considered 'easy' in a sense that you could sketch a proof of it while explaining the stamement to undergrads than there is also a question if this easy reformulation can be proved in Lean. Explicitly, I would say that such easy reformulations are:
For RH: can we prove that the zeta-function extends to the critical strip?
For Poincare: can we prove that a compact oriented 3-manifold is homotopy equivalent to a sphere iff its simply connected and is homology sphere? (I think this is not hard in maths, just a consequence of Hurewicz theorem, but I might be mistaken). Can we at least prove that the 3-sphere is compact oriented and simply connected?
For BSD: can we define a modular elliptic curve and prove that its L-function extends to the whole complex plane?
For P=NP: can we define an NP-complete problem and prove that P=NP iff 3SAT is in P?
For Hodge conjecture: can we state it in such a way that we can prove that the fundamental class of an algebraic subvariety is a Hodge class?

[Adam Topaz]

IMO the statement of the Hodge conjecture is a long long LONG way from being formalizable

[Joachim Hauge]

Adam Topaz said:

IMO the statement of the Hodge conjecture is a long long LONG way from being formalizable

Would the Tate conjecture be easier?

[Adam Topaz]

I was going to immediately say "NO!" but maybe the answer is actually yes?!

[Adam Topaz]

I mean if one sets up etale cohomology in the right way then the Tate conjecture can be stated just as a consequence of the basic properties of cohomology (functoriality)

[Adam Topaz]

Ah, but one would need cycle classes as well. For divisors it would be easier to state as you just need the relationship between H^1 and Pic.

[Kevin Buzzard]

@Stepan Nesterov For BSD one can define a modular elliptic curve in theory (although it would be some work), but the statement of BSD is not about modular elliptic curves, it is about elliptic curves, because it is a gigantic theorem (which implies FLT) that all elliptic curves are modular.

[Kevin Buzzard]

The other issue with modular elliptic curves is that there are five equivalent definitions, and to prove they're equivalent one has to use Faltings' theorem which is another huge batch of algebraic geometry and analysis and number theory (which won him a Fields medal).

[Kevin Buzzard]

So one has to be very careful here about what one really means. If P <-> Q is proved by mathematicians then even if the proof is thousands of pages, all mathematicians instantly now regard P and Q as being equal and can happily just invoke this equality at any time, e.g. when stating other conjectures.

[Stepan Nesterov]

Kevin Buzzard said:

Stepan Nesterov For BSD one can define a modular elliptic curve in theory (although it would be some work), but the statement of BSD is not about modular elliptic curves, it is about elliptic curves, because it is a gigantic theorem (which implies FLT) that all elliptic curves are modular.

Right, and it is ridiculous to think that one just sit and formalize the proof of the modularity theorem right now, so I would settle for accepting it as it is and just ask for the definitions of the L-function, conductor, canonical height, elliptic regulator and the Tate-Shafarevich group.

[Kevin Buzzard]

The official statement of the Clay problem is only about weak BSD so one doesn't need any conductor, height, regulator or Sha.

[Stepan Nesterov]

Kevin Buzzard said:

The other issue with modular elliptic curves is that there are five equivalent definitions, and to prove they're equivalent one has to use Faltings' theorem which is another huge batch of algebraic geometry and analysis and number theory (which won him a Fields medal).

But we don't need the hard direction to prove that L-function has the meromophic continuation, if I am not mistaken

[Kevin Buzzard]

The work is in showing that the definitions are equivalent, so right now we are not discussing how hard it is to prove that the L-function has AC if the curve is modular, we are discussing what "the curve is modular" _means_.

[Kevin Buzzard]

The issue is that the geometric definitions (quotient of a modular curve) only follow from the algebraic definitions ("a_p match up") if you know Faltings' isogeny theorem.

[Kevin Buzzard]

Because Faltings' theorem is a theorem, mathematicians no longer have any interest in this question, but it's still there if you're thinking about it from a formalisation point of view. This is the problem -- mathematicians can use anything in our literature; if you don't have access to that then there might be more than one say to state the conjecture. The "easiest" way is far easier than the "hardest" way; on the other hand if you go with the easiest way then you're at risk of being accused of not having formalised "the conjecture" (whatever that means) correctly.

[Kevin Buzzard]

The easiest way is literally to formalise the absolute minimum number of defs and then just throw in every result you need as part of the conjecture, for example one makes the assertion that the algebraic rank is finite part of the conjecture, even though this is classical and almost 100 years old (but will still be hard work to formalise!)

[Kevin Buzzard]

Algebraic rank finite ($E(\mathbb{Q})$ f.g. ab gp) is something I have lectured many times to the MSc students at Imperial, but it has not been formalised in any theorem prover.

[Stepan Nesterov]

Right, you have a point here. I agree that there are aspects of this which are incredibly hard and will not be in any prover soon, but I am still curious which aspects already are.

[Stepan Nesterov]

Are easy implications 'E is a quotient of a modular curve' => 'L(E,s)=L(f,s) for a new eigenform of weight 2' => 'L(E,s) has an entire continuation' formalised? If not, which theories and definitions are currently missing?

[Kevin Buzzard]

The answer to "which aspects already are" is easy for BSD: the group structure on a plane cubic has been defined, and proved to be commutative, in Coq; the definition of a modular form is in no prover, finite generation of rational points is in no prover, definition of L-function is in no prover, everything else is in no prover.

[Kevin Buzzard]

I think you are hugely overestimating exactly what has been going on in this area for the last 50 years (as I did when I entered the area -- I was shocked).

[Kevin Buzzard]

Everything is missing. Modular forms are in no prover. Modular curves are in no prover. Maps between algebraic varieties are in no prover. L-functions of any object other than abelian objects (Dirichlet characters) are in no prover.

[Adam Topaz]

Kevin Buzzard said:

... Maps between algebraic varieties are in no prover. ...

:sad:

[Kevin Buzzard]

I made schemes with a bunch of undergraduates in Lean and then asked how it was done in the other provers and was shocked to the core when I found out that nobody had done anything like it in any other prover. It took a while to formalise the definition and prove affine schemes were schemes, but it was relatively straightforward (given the massive amount of help I got from this chat) and a whole lot of fun. I am a number theorist and would love to be doing the stuff you're talking about -- my PhD was on modular forms -- but everything takes a lot of time. I have got someone in London thinking about modular forms (Chris Birkbeck), and I think Heather and Alex Kontorovich are thinking about them too. I will have a project student thinking about elliptic curves in June. The problem with "random people doing it" is that often their work doesn't end up in mathlib; indeed our initial schemes work did not end up in mathlib, and it took several years before a 3rd generation definition made it into the library. We're having a lot of fun, but progress is slow simply because we don't have enough people and not enough of those that we have are trained to write code which is professional enough to make it into mathlib.

[Johan Commelin]

I definitely think that stating Tate is a lot easier than stating Hodge. Probably the difference between 1 year of hard work and 5 years of hard work.

[Kevin Buzzard]

How about this for a well-defined question. How hard would it be to state a minimal version of each of the problems? By this I mean: no sorried defs, but as many sorried theorems as you like. For example for BSD we have to define the addition, negation and identity on the rational solutions of $y^2=$ cubic in $\Z[X]$ + $\{\infty\}$, and then we can sorry the following: (1) it's an abelian group (2) it's finitely-generated. Similarly for the L-function we can define a_p for all primes not dividing 2*discriminant, sorry the theorem that the product converges for Re(s)>1.5 or even Re(s)>2 which is much easier (we can ignore the bad primes because it's only weak BSD), sorry the theorem that there's analytic continuation (a good example of a theorem for which no living person knows all the details of the full proof, at least in my opinion, because all known proofs involve hard analysis and hard geometry and hard number theory), sorry the theorem that the order of vanishing at s=1 is finite (because we don't have any complex analysis so we even have to sorry this) and then we can state the conjecture. This would be a great student project (and I have a student in mind) and easily accessible in Lean. We don't sell it as "this is an extremely poor attempt at formalising BSD", we sell it as "this is a level of a puzzle game and if you complete all the levels then you've proved BSD", which is true.

[Kevin Buzzard]

I will give this to the student who's working with me on a project; as far as I can see the only hurdles are (1) do we have infinite products? (2) can we say "this function from the subspace Re(s)>1.5 of C to C is holomorphic"? (3) can we take the complex derivative of a holomorphic function C -> C and get a function C -> C? We can sorry the assertion that it's holomorphic. I know very little about the analysis side of the library.

[Kevin Buzzard]

With this kind of attitude, RH would be straightforward to state, BSD will be done within a couple of months, Yang Mills isn't a maths question, and I do not feel that I understand enough about the library to be able to comment on the other four problems.

[Sebastien Gouezel]

RH is already straightforward to state: it is equivalent to the fact that the counting function for primes is $li(x) + O(x^{1/2+\epsilon})$ for any positive $\epsilon$ (i.e., the fluctuations in the primes are just like in the central limit theorem), and we have all this in mathlib.

[Stepan Nesterov]

Kevin Buzzard said:

How about this for a well-defined question. How hard would it be to state a minimal version of each of the problems? By this I mean: no sorried defs, but as many sorried theorems as you like. For example for BSD we have to define the addition, negation and identity on the rational solutions of $y^2=$ cubic in $\Z[X]$ + $\{\infty\}$, and then we can sorry the following: (1) it's an abelian group (2) it's finitely-generated. Similarly for the L-function we can define a_p for all primes not dividing 2*discriminant, sorry the theorem that the product converges for Re(s)>1.5 or even Re(s)>2 which is much easier (we can ignore the bad primes because it's only weak BSD), sorry the theorem that there's analytic continuation (a good example of a theorem for which no living person knows all the details of the full proof, at least in my opinion, because all known proofs involve hard analysis and hard geometry and hard number theory), sorry the theorem that the order of vanishing at s=1 is finite (because we don't have any complex analysis so we even have to sorry this) and then we can state the conjecture. This would be a great student project (and I have a student in mind) and easily accessible in Lean. We don't sell it as "this is an extremely poor attempt at formalising BSD", we sell it as "this is a level of a puzzle game and if you complete all the levels then you've proved BSD", which is true.

But then we don't have a reason to stop and not formulate the strong BSD also, right?

If we define the naive height H(x,y)=max(absolute value of numerator and denominator of x), define the canonical height as the quadratic form on E(Q) such that stuff, sorry that is exists and is unique, and sorry the finiteness of Ш, we're probably good to go, I guess.

[Kevin Buzzard]

I think that formulating strong BSD will be much harder, because defining Sha (even as a set) will be hard work because we have no varieties, defining the period integrals will be hard work because we have no theory of complex integration in Lean, defining the fudge factors will involve implementing Tate's algorithm etc. Mathlib is not ready for this yet, but it's definitely ready for weak BSD modulo the issues I flagged above, which I suspect will all be easily solvable. Strong BSD is something which a competent Lean user would really have to "take on" and put a lot of time into.

[Kevin Buzzard]

Weak BSD I think I can give to a mathematician with very little Lean experience (and indeed I just did, I just sent Jamie Bell an email proposing this)

[Stepan Nesterov]

If we have Galois groups, we can just define Ш as a subset of H^1(G_K,E(K^{alg})) via cocycles stuff

[Stepan Nesterov]

And I guess the integration is just dx/y over the real points of E, although this requires the variable change formula to include infinity, which mathlib might not have (?)

[Kevin Buzzard]

We don't have infinite Galois groups, and even if we did it might be quite a challenge to prove that G_K acts on the group E(K^alg), although I guess if we're allowed sorries everywhere then it might be feasible. We do not have any theory of contour integration at all. You write G_K but if K isn't Q we don't have any theory of completing K at a prime ideal to impose the local conditions. We don't even have an undergraduate curriculum yet -- there are many holes in mathlib right now. You are optimistic but I can see the extent of the work involved and it is pretty large, even with sorries everywhere.

[Stepan Nesterov]

Kevin Buzzard said:

We don't have infinite Galois groups, and even if we did it might be quite a challenge to prove that G_K acts on the group E(K^alg), although I guess if we're allowed sorries everywhere then it might be feasible. We do not have any theory of contour integration at all. You write G_K but if K isn't Q we don't have any theory of completing K at a prime ideal to impose the local conditions. We don't even have an undergraduate curriculum yet -- there are many holes in mathlib right now. You are optimistic but I can see the extent of the work involved and it is pretty large, even with sorries everywhere.

Right, you need decomposition groups to define Sha, which take work to define in order to sorry that all of them are conjugate

[Stepan Nesterov]

And we need topology on G_K to define a cocycle correctly

[Stepan Nesterov]

Yes, on second thought, maybe we can't just sorry finiteness of Ш :(

[Kevin Buzzard]

I think that asking hard questions like this are the correct way to drive mathlib forward in a direction which will make it more appealing to mathematicians. I think the idea of formalising the statement of strong BSD is a great one.

In my not so humble opinion, here is what I think is one of the underlying problems with this entire computer theorem proving area. Until recently it was mostly dominated by computer scientists, most of whom neither know nor care about the strong BSD conjecture. The kind of mathematics which was being formalised was completely random as a consequence of this; people would try something, and if it turned out to look difficult they'd give up and try something else which they could manage because they needed their next paper. So you look through the literature and see totally random useless stuff formalised, and easy stuff being formalised several times, and so on. You want to formalise the work of a Fields Medallist? Let's choose John Thompson because Feit and him proved a theorem about finite groups whose proof just used a whole bunch of other theorems about finite groups, and finite groups are easy to define in a theorem prover. With this attitude the area was growing in a really unappealing and uninteresting way. Occasionally some good stuff would get done, e.g. odd order or PNT or Kepler, but for the most part these were proofs involving elementary objects, and to a certain extent this reflected the mathematical interests or abilities of those doing the formalising. Lean aims to change all that, by working on things which are much too hard to do in Lean or any other prover like strong BSD, and then distilling out from that various things which can be done and, because they're related to strong BSD, a "trendy" thing, are of inherent interest to young mathematicians watching this area and trying to figure out what is going on. But you don't get something for nothing -- formalising strong BSD will be hard work. But the para above explains why I really think it's worth it.

[Adam Topaz]

FWIW @Stepan Nesterov a project which could be started on with mathlib right now is to define absolute Galois groups as profinite groups. But this would be a project!

[Kevin Buzzard]

It would be a really nice project in fact. Do we have separable closures?

[Johan Commelin]

I don't think so, but it shouldn't be hard, now that we have algebraic closures and separable extensions

[Johan Commelin]

Do we want infinite Galois theory in general, instead of just absolute Galois groups? That seems like the right approach to me.

[Kevin Buzzard]

How about one defines the infinite Galois group of an algebraic, normal, separable extension as the automorphisms, proves that the natural map from this to the projective limit of finite Galois groups is an isomorphism of groups, and pulls back the topology?

I guess the real project (which would take a while) would be to deduce the infinite FTG from the finite one. I once did this on paper and it's harder than you think, either that or I was using a crappy reference and/or making it up and missing shortcuts.

[Kevin Buzzard]

I had a job finding a reference. I have a pdf somewhere, not on this laptop though.

[Kevin Buzzard]

Of course if you're just after Sha you don't need any of this, you just need the topology on the abs Gal gp so you can write down continuous cocycles.

[Adam Topaz]

I think the correct approach here is to develop some theory for Profinite groups in general first. E.g. show that a Profinite group is the limit of its finite continuous group quotients, and give a description of the closed subgroups in terms of compatible systems of subgroups of the finite quotients. The infinite Galois correspondence should follow without too much trouble from the finite one with a good API of this sort

[Mario Carneiro]

Sebastien Gouezel said:

RH is already straightforward to state: it is equivalent to the fact that the counting function for primes is $li(x) + O(x^{1/2+\epsilon})$ for any positive $\epsilon$ (i.e., the fluctuations in the primes are just like in the central limit theorem), and we have all this in mathlib.

There are a number of simple formulations of RH at this MO question, including the linked answer which can be stated in a handful of lines of lean without even using mathlib.

[Jz Pan]

IIRC if you assume an elliptic curve $E/\mathbb{Q}$ has full rational 2-torsions, say $y^2=x(x-e_1)(x-e_2)$, you can define an element of 2-Selmer group, as a curve in $\mathbb{P}^3$, in purely elementary way, and hopefully you can prove that for any $p\nmid 2e_1e_2(e_1-e_2)\infty$, such curve have a solution in $\mathbb{Q}_p$ by only using Hensel's lemma, etc. So you can prove the weak Mordell-Weil theorem.

[Stepan Nesterov]

Jz Pan said:

IIRC if you assume an elliptic curve $E/\mathbb{Q}$ has full rational 2-torsions, say $y^2=x(x-e_1)(x-e_2)$, you can define an element of 2-Selmer group, as a curve in $\mathbb{P}^3$, in purely elementary way, and hopefully you can prove that for any $p\nmid 2e_1e_2(e_1-e_2)\infty$, such curve have a solution in $\mathbb{Q}_p$ by only using Hensel's lemma, etc. So you can prove the weak Mordell-Weil theorem.

Yes, and if we know Dirichlet's unit theorem, then we get the general case by that method.

[Stepan Nesterov]

Applied over a number field $K$ where the 2-torsion is rational.

[Kevin Buzzard]

This is correct, but it's not enough for strong BSD. There are concrete models for n-torsion for n<=5 and abstract models for all n, but each model is for a fixed n and for Sha you have to do all n at once.