Project public

Stream: FLT

[Kevin Buzzard]

So the project is now public: here is the repo and here is a blog post. I want to watch the snooker am too tired to do any more today, but tomorrow I'll post the first "things which it's possible to do right now" post, following the Tao/Kontorovich model of leading a formalisation project.

One thing I'm a bit bewildered by right now is that the switch from private to public has made my link to the blueprint stop working. All the links on the blog post are fine, e.g.

https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_document.html

for the graph and

https://imperialcollegelondon.github.io/FLT/blueprint/index.html

for the LaTeX, and I can manufacture this link

https://imperialcollegelondon.github.io/FLT/

to some home page (which says Fermat's Last Theorems?! How do I fix that? Sometimes there's no s's and now there are two?)

But the "blueprint" link at https://imperialcollegelondon.github.io/FLT/ and the link at the top of the README on the github project page don't work for me(fixed by removing a cookie -- thanks Patrick)

[Patrick Massot]

Kevin I wrote you a PM message one hour ago explaining what you need to do.

[Patrick Massot]

In particular the issue you see won’t be seen by other people, this is purely your navigator trying to be too helpful.

[Julian Berman]

(The one character fix for Theorems is https://github.com/ImperialCollegeLondon/FLT/pull/26 )

[Alex Kontorovich]

Oh! I must have the same cookie issue (I must've clicked it just as it went live, and gotten the old cookie?). Do you have to clear all cookies, or is there another way to do it?

[Kevin Buzzard]

Patrick Massot said:

You need to tell your navigator to purge github.io cookies

[Ruben Van de Velde]

Wait, FLT is all green, are you done? :)

[Mario Carneiro]

One suggestion: I think the main theorem should be in FLT.lean i.e. the root file. Currently the root file contains

import FLT.Basic.Reductions
import FLT.EllipticCurve.Torsion
import FLT.for_mathlib.Coalgebra.Monoid
import FLT.for_mathlib.Coalgebra.Sweedler
import FLT.for_mathlib.Coalgebra.TensorProduct
import FLT.for_mathlib.HopfAlgebra.Basic
import FLT.GaloisRepresentation.HardlyRamified
import FLT.GroupScheme.FiniteFlat
import FLT.Hard.Results
import FLT.TateCurve.TateCurve

and it's not particularly obvious to determine where the main theorem is

[Mario Carneiro]

Alternatively, if the project also contains consequences of FLT such that putting it in the last file is awkward, this would be a good use for the recall command

[Kevin Buzzard]

FLT has no consequences

[Kevin Buzzard]

other than finishing Freek's list

[Floris van Doorn]

it's even in the name... :smile:

[Floris van Doorn]

Someone once jokingly told me a proof that $\sqrt[n]{2}$ is irrational:

For $n=2$ the result is standard, and for $n\ge3$ we can rewrite $\sqrt[n]{2}=\frac{p}{q}$ as $q^n+q^n=p^n$, which has no nontrivial solutions by FLT.

[Ruben Van de Velde]

That's the argument Kevin suggested while I was proving FLT3

[Julian Berman]

Floris van Doorn said:

Someone once jokingly told me a proof that $\sqrt[n]{2}$ is irrational:

For $n=2$ the result is standard, and for $n\ge3$ we can rewrite $\sqrt[n]{2}=\frac{p}{q}$ as $q^n+q^n=p^n$, which has no nontrivial solutions by FLT.

That's one of the examples in the (famous?) "overpowered theorems to solve simple problems" thread on MathExchange or overflow or wherever that thread is, right?

[Julian Berman]

Yeah this one -- https://mathoverflow.net/questions/42512/awfully-sophisticated-proof-for-simple-facts -- looks like Kevin is in the comments though not for the FLT one.

[Floris van Doorn]

I've seen that thread before, but rereading it is still amazing.

[Floris van Doorn]

That thread is full of challenges of minimizing unnecessary imports in Mathlib: if we can formalize these crazy proofs without having imported the standard version, we have succeeded with minimizing imports :grinning_face_with_smiling_eyes:

[David Michael Roberts]

@Kevin Buzzard You can fix the problem with the "canonical" isomorphisms by saying there is a canonical Z/2-torsor of "canonical" isomorphisms , no? :-)

[Scott Carnahan]

I haven't read it in depth yet, so I'm a little unclear on the big picture. Is the modularity lifting theorem (4.1) the part that lets you avoid Ribet's level-lowering?

[Patrick Massot]

Ruben Van de Velde said:

Wait, FLT is all green, are you done? :)

For people who actually wonder: this is the difference between green and dark green. What is currently formalized is that FLT follow from other nodes. But those nodes are not all formalized.

[Patrick Massot]

Floris van Doorn said:

That thread is full of challenges of minimizing unnecessary imports in Mathlib: if we can formalize these crazy proofs without having imported the standard version, we have succeeded with minimizing imports :grinning_face_with_smiling_eyes:

I didn’t read it again but I saw it in the past and, if I remember correctly, most of the proofs mentioned there are actually circular (or very nearly circular in the sense that a very early lemma using in the big gun proof immediately imply the target).

[Johan Commelin]

Going back to @Mario Carneiro 's suggestion: I agree that it would be good to make obvious in the main file where the main statement is. Either using recall or via a comment pointing to an optimized-for-uninitiated-consumption Lean file

[Ruben Van de Velde]

Patrick Massot said:

Ruben Van de Velde said:

Wait, FLT is all green, are you done? :)

For people who actually wonder: this is the difference between green and dark green. What is currently formalized is that FLT follow from other nodes. But those nodes are not all formalized.

I was about to suggest it needed a legend when I noticed it has one :sweat_smile:

[Yaël Dillies]

Re: FLT.lean. It would be good to have #11853 merged

[Kevin Buzzard]

Scott Carnahan said:

I haven't read it in depth yet, so I'm a little unclear on the big picture. Is the modularity lifting theorem (4.1) the part that lets you avoid Ribet's level-lowering?

Wiles also used a modularity lifting theorem (in fact he invented the idea). Ours is "better" but in some sense the reason we can avoid Ribet is just because we go a different way.

Given a counterexample to FLT you can make this dubious-looking semistable elliptic curve E called the Frey curve, whose p-torsion had conductor 2 (very small). Wiles did: E[3] modular (by hard analysis) => E modular (by modularity lifting theorem) => E[p] modular (trivial) => E[p] modular of level 2 (Ribet) => contradiction. A bit more precisely, "E modular" means "E comes from a modular form of some random large level" and there exist plenty of modular forms of random large level so at some point you have to get control of the level to get the contradiction, and this is what Ribet does. The reason the argument goes in this order is that at that time nobody knew what to do with "E[p] has small conductor" to get a contradiction, other than "E[p] is modular" and then "Ribet says that if it's modular, it's modular of level = conductor".

But now we can do other things with E[p]. For example, after Taylor/Khare-Wintenberger (which relies on a bunch of other stuff including hard analysis and a fancier modularity lifting theorem which works for Hilbert modular forms) we can lift E[p] to some family of ell-adic Galois representations all of which have small conductor, and the observation of Taylor is that we can now specialise this family at 3 and reduce mod 3 to get a mod 3 representation of suspiciously small conductor; Taylor discovered a way to prove that this can't exist, via an explicit numerical calculation which relies on the fact that 3 is small and which wouldn't work at p (which is the p in a^p+b^p=c^p so could be gigantic).

[Kevin Buzzard]

Mario Carneiro said:

One suggestion: I think the main theorem should be in FLT.lean i.e. the root file. Currently the root file contains

import FLT.Basic.Reductions
import FLT.EllipticCurve.Torsion
import FLT.for_mathlib.Coalgebra.Monoid
import FLT.for_mathlib.Coalgebra.Sweedler
import FLT.for_mathlib.Coalgebra.TensorProduct
import FLT.for_mathlib.HopfAlgebra.Basic
import FLT.GaloisRepresentation.HardlyRamified
import FLT.GroupScheme.FiniteFlat
import FLT.Hard.Results
import FLT.TateCurve.TateCurve

and it's not particularly obvious to determine where the main theorem is

So I don't need a stupid file containing all the names of all the other files? That's great.

I have FLT_statement.lean which isn't in that list for some reason (I think the list was auto-generated?) but which contains a statement of PNat.pow_add_pow_ne_pow . So you're suggesting I just move this to FLT.lean and dump the stupid file? I want it so that lake build just always builds all the Lean files in FLT/ and the simpler the set-up the better.

[Adam Topaz]

You could just make that FLT_statement file a default target

[Mario Carneiro]

For building all the files in FLT/, you can use globs in the lakefile

[Mario Carneiro]

looks like you are already doing that

[Mario Carneiro]

PS: once you bump to (a mathlib on) 4.8.0-rc1, you will want to ditch the -DwarningAsError=true line from the lakefile and use --wfail in the lake invocations in CI instead

[Mario Carneiro]

...I guess the line isn't being used in the first place

[Mario Carneiro]

Question: why is Wiles--Taylor-Wiles called that? I'm pretty sure there aren't two Wiles's in this story...

[Adam Topaz]

It’s work of Wiles together with (joint) work of Taylor-Wiles

[Adam Topaz]

The story is essentially: Taylor-Wiles repaired a gap in Wiles

[Mario Carneiro]

I would have thought that means the whole work is Taylor-Wiles

[Adam Topaz]

In my experience the way people give attribution in such situations is on a case-by-case basis. Kevin probably knows precisely why it’s the case here

[Ruben Van de Velde]

The main part of the proof was in an article by Wiles alone, and the final gap was filled in the accompanying article by Taylor and Wiles

[David Michael Roberts]

I don't know the nitty-gritty, but note saying Taylor–Wiles implies in some citation cultures outside pure maths that Taylor was the lead author. The double attribution draws attention to the two separate but simultaneous papers, while acknowledging that Wiles did the lion's share and was really 'first'

[Mario Carneiro]

It's not actually clear to me whether Wiles did the "lion's share" though. From what I've heard from interviews and such a lot of it was building on earlier work, in particular a result of Ribet's. Wiles's proof was just the "last part" in that sense. But I am definitely in no position to make any reasonably accurate estimates of how much of the proof is Wiles's.

[Adam Topaz]

This wiki page has quite a good summary IMO: https://en.m.wikipedia.org/wiki/Wiles%27s_proof_of_Fermat%27s_Last_Theorem

[Mario Carneiro]

In 2005, Dutch computer scientist Jan Bergstra posed the problem of formalizing Wiles's proof in such a way that it could be verified by computer.[24]

Looks like that page needs an update :)

[Mario Carneiro]

I have heard the general story of FLT before, but the part that this doesn't tell me is how big and hard the theorems actually are. It could be that Ribet's theorem is 1 page and Wiles's is 1000 or vice versa, but due to the nature of history it's the one who does the last part that gets the credit. (I'm not actually saying that I know that this happens in this case, only that the usual way this historical information is presented doesn't make it obvious.) The classification of finite simple groups is even more obviously the joint work of many parties contributing very different page counts to the full proof, if it could all be put in one place. One nice outcome of this FLT project is that it will be easy to see the relative magnitudes of contributions to the FLT, not just Wiles's proof but also its prerequisites. (Although I am aware that the original project description intends to put off those prerequisites until last.)

[Kevin Buzzard]

Wiles' paper introduced several key new ideas, one of which doesn't quite work, but the single author paper was 100+ pages long. Ribet's paper was about 30 pages long

[Kevin Buzzard]

Some of the references are certainly more than 100 pages long (eg probably Mazur)

[Mario Carneiro]

Do you know the complete list of references which in principle would take us from mathlib to FLT?

[Mario Carneiro]

Put another way, do you have a list (or at least a clear sense) of all the sorries you plan to group under "results known in the 1980's that we won't be formalizing for v1"

[Kevin Buzzard]

I would say I know a covering set of references, in the sense that one thing I think I have done is got some kind of (private) 15 page document which I'm slowly moving over to the blueprint and which reduces FLT to results from the 80s, but the referencse also have references. Much of what is needed has been dumped in chapter top but we still can't even state many of these results in Lean. I'm working on a project this weekend which will get us closer to stating one of them though.

[Scott Carnahan]

Overheard in Berkeley ~20 years ago: "If it weren't for my daddy, Andrew Wiles would still be locked in his attic."

[Kevin Buzzard]

Ken's kids were 4 and 2 when I was there

[Kim Morrison]

There's also the complication that the formalization planned here relies less on Ribet than the original proof.

[David Michael Roberts]

Mario Carneiro said:

It's not actually clear to me whether Wiles did the "lion's share" though.

I mean out of the package of work that went from "publicly-known in 1992" to the proof of FLT. Clearly, if you want to import all prior results, where do you draw the line? The work of Grothendieck on the 60s? Of Weil in the 40s? Of Hecke in the 20s? Not to mention Ribet, Serre, Langlands, Shimura, Taniyama,....

Taylor–Wiles is 20 pages (5 pages of which were an alternate proof supplied by Faltings that simplifies part of the argument), Wiles solo is about 110 pages.

[Mario Carneiro]

Personally, I prefer to draw the line based on the topic, not the historical tradition. It's still a judgment call how much of the prerequisites are considered part of FLT proper and not some background theory, but one way to get such a line is to see how much ends up in the FLT repo vs upstream

[David Michael Roberts]

We just have different denominators for who contributed how much to what :-)

[Kim Morrison]

I'm not super confident about using the FLT vs upstream divide... Actually, has anyone (@Kevin Buzzard?) even ball park estimated the LoC of a complete proof relative to where we are now? I'm guessing it is a 10^6 number (i.e. another Mathlib), not a 10^5 number.

[Eric Wieser]

Isn't mathlib a 10^7 number?

[Ruben Van de Velde]

Do you count #align? :)

[Kevin Buzzard]

I have not attempted to estimate LOC. I've attempted to estimate number of pages and maybe 2000 is a ballpark estimate but as we saw in LTE five lines can take anything between five minutes and one year

[Kim Morrison]

I meant that Mathlib is about 1.5 * 10^6 LoC, and I wouldn't be surprised if FLT will require another 10^6.

[Kevin Buzzard]

A full proof of FLT might be another 10^6, but it's not clear to me that the majority of these 10^6 will pass through the FLT repo. My vision (and I don't think I'm being over-optimistic here) is that within a few years FLT contains most of (and mathlib contains the rest of) a proof of an R=T theorem and a proof of FLT using it, modulo a bunch of huge concrete sorries (with no data sorried) of the form "well we need this result which says that if $E/\mathbb{Q}$ is an elliptic curve then $E(\mathbb{Q})^{tors}$ has size at most 16 but this is 100 pages and there's no reason for development of this theorem to be in the FLT repo".

[Joël Riou]

In the blueprint (section 7.6), it seems that étale cohomology is part of the proof https://imperialcollegelondon.github.io/FLT/blueprint/ch_bestiary.html#a0000000033 (i.e. the Galois representations that are involved are not just Tate modules of abelian varieties), as at least some $H^2$ appears. Then, the part of the general étale formalism which is needed should probably develop in mathlib rather than in the FLT repository, unless some important general étale theorems are sorried (these are 1960s mathematics...), in which case the consequences of these would have to be in the FLT repository.

[Kevin Buzzard]

I wonder whether the original proof of FLT could have got away with just Tate modules of Jacobians. But the proof I'm formalising will necessarily need to consider the $\ell$-adic etale $H^2$ of a smooth proper surface over a global field (with constant coefficients). So yes we need etale cohomology, you're right.

[Kevin Buzzard]

FLT#53

[Adam Topaz]

Do you care if ell-adic cohomology of X : Scheme.{0} has universe level 1?

[Kevin Buzzard]

Mario Carneiro said:

One suggestion: I think the main theorem should be in FLT.lean i.e. the root file. Currently the root file contains

import FLT.Basic.Reductions
import FLT.EllipticCurve.Torsion
import FLT.for_mathlib.Coalgebra.Monoid
import FLT.for_mathlib.Coalgebra.Sweedler
import FLT.for_mathlib.Coalgebra.TensorProduct
import FLT.for_mathlib.HopfAlgebra.Basic
import FLT.GaloisRepresentation.HardlyRamified
import FLT.GroupScheme.FiniteFlat
import FLT.Hard.Results
import FLT.TateCurve.TateCurve

and it's not particularly obvious to determine where the main theorem is

I've now tried this and according to my experiments it broke leanblueprint, which now doesn't know which Lean files to import to find the declarations I mention in the LaTeX. How should I fix this? Right now I have a hack in line 1 of FLT.lean. I would love to rid my repo of the "list of everything" file and have lake build just mean "build FLT.lean and all the files in FLT/"

[Mario Carneiro]

There should not be any FLT files not transitively reachable from the root, for basic "no dead code" reasons

[Mario Carneiro]

you don't need the FLT file to actually be a list of everything for this to be true

[Mario Carneiro]

The blueprint itself is presumably a connected DAG with FLT as the terminal node, so just make sure the imports reflect that structure

[Kevin Buzzard]

Mario Carneiro said:

PS: once you bump to (a mathlib on) 4.8.0-rc1, you will want to ditch the -DwarningAsError=true line from the lakefile and use --wfail in the lake invocations in CI instead

I have been putting off bumping because people were saying that the cache wasn't working and there was talk of there going to be an rc2 etc etc, so I didn't know when it was safe to bump.

[Mario Carneiro]

That's fair, I agree it's a bit unstable

[Mario Carneiro]

(it is a double feature release after all)

[Kevin Buzzard]

Adam Topaz said:

Do you care if ell-adic cohomology of X : Scheme.{0} has universe level 1?

Nice question! The scheme X is smooth and proper over a number field K which we can assume to be in Type (it would certainly have to work with input Rat : Type) and in maths I can prove that the ell-adic H^2(X/K,Q_ell) is a finite-dimensional continuous Galois rep. Is this enough to descend? I think it is, the proof of finite-dimensionality gives me (noncomputably) a basis over Q_ell (in Type) indexed by Fin N(in Type) and then the rep is uniquely encoded by the resulting function from Gal(K-bar/K) (in Type) to square matrices over Q_ell indexed by Fin N (in Type). So can read off that information, reconstruct the Galois rep and then even prove that the lift back up to Type 1 will be isomorphic to the answer you gave me.

[Kevin Buzzard]

Mario Carneiro said:

The blueprint itself is presumably a connected DAG with FLT as the terminal node, so just make sure the imports reflect that structure

I definitely don't want to assume my blueprint is connected or that my code is connected. Right now I am working on an example of an automorphic form because I thought it would be cool to construct a nontrivial one. We definitely don't need this example for FLT!

[Chris Birkbeck]

Kevin Buzzard said:

Mario Carneiro said:

The blueprint itself is presumably a connected DAG with FLT as the terminal node, so just make sure the imports reflect that structure

I definitely don't want to assume my blueprint is connected or that my code is connected. Right now I am working on an example of an automorphic form because I thought it would be cool to construct a nontrivial one. We definitely don't need this example for FLT!

We have non-trivial modular forms, so done! :p

[Ruben Van de Velde]

I can look at bumping mathlib later

[Joël Riou]

Adam Topaz said:

Do you care if ell-adic cohomology of X : Scheme.{0} has universe level 1?

Depending on how exactly we proceed and how many theorems we are able to prove at a given time, it may even be in Type 2 if we make no particular effort! One universe bump is because the étale site of X : Scheme.{0} is a large category (a possible fix at least for noetherian X is to replace the étale site with a small one with equivalent categories of sheaves, so that we may consider categories of sheaves of AddCommGroupCat.{0} instead of AddCommGroupCat.{1} which would otherwise be necessary to get a sheafification functor). The second universe bump is because the category of étale sheave with values in AddCommGroupCat.{1} has a type of objects in Type 2, and then Ext-groups of sheaves (resp. Homs in the derived category) are going to be in Type 2 until we show there exists injective (resp. K-injective) resolutions.

In any case, we may shrink to Type 0 afterwards because of finiteness theorems as Kevin said. Let us not focus on this now!

[Mario Carneiro]

Kevin Buzzard said:

Mario Carneiro said:

The blueprint itself is presumably a connected DAG with FLT as the terminal node, so just make sure the imports reflect that structure

I definitely don't want to assume my blueprint is connected or that my code is connected. Right now I am working on an example of an automorphic form because I thought it would be cool to construct a nontrivial one. We definitely don't need this example for FLT!

From the sounds of things, although lake will compile all files due to the glob, the blueprint will only consider definitions to exist if they are reachable from the main file. So if you want to have a definition that shows up in the blueprint, it should be in a file which is imported by something, either the main file or some file which you think will need to eventually reference it.

[Kevin Buzzard]

So Leanblueprint will only use FLT.lean and what it imports, so if I am working on an example which will not be logically necessary for the proof but might be instructional for the reader then I can't document it without adding an artificial import somewhere. I thought FLT.lean looked quite good with only one import. Should I put it in the file it imports or something?

[Kevin Buzzard]

@Patrick Massot do you have any comments?

[Mario Carneiro]

yes, the fallback would be to put the import in the FLT.lean file but I can see that this might be untidy. Maybe something can be done on the leanblueprint side, I'm not sure how it is configured

[Mario Carneiro]

Another possibility would have another lean_lib like FLTExtras which imports FLT and also random assorted other files, and which is used as the root for leanblueprint purposes

[Patrick Massot]

Mario Carneiro said:

the blueprint will only consider definitions to exist if they are reachable from the main file. So if you want to have a definition that shows up in the blueprint, it should be in a file which is imported by something, either the main file or some file which you think will need to eventually reference it.

Yes, this is correct. It seems reasonable to me. I don’t really see another way this should work, but I am open to suggestions.

[Mario Carneiro]

The alternative would be to get leanblueprint to also use a glob import

[Patrick Massot]

It currently uses you code (tweaked by Mac to work on 4.8.0) at https://github.com/PatrickMassot/checkdecls/blob/master/Main.lean.

[Mario Carneiro]

oh lovely, it's already using the lake API, so it shouldn't be hard to make it use the globs

[Matthew Ballard]

Late to the previous discussion but here’s a free (after registering) 1995 NYT article about the state of FLT

[Matthew Ballard]

Scott Carnahan said:

Overheard in Berkeley ~20 years ago: "If it weren't for my daddy, Andrew Wiles would still be locked in his attic."

Speaking of stories from school, I was once told that Wiles was asked during a TV interview what the biggest challenge to proving FLT's theorem was. The "claim" was that his response was to hold up a picture of a faculty member from my undergraduate institution.

[Matthew Ballard]

I am sure it wasn't true but what did I know as < 20 year old.