Outstanding Tasks, V1

Stream: FLT

[Kevin Buzzard]

So let me stress that I still have a day job, with exam invigilation and marking, supervising undergraduate projects etc etc; term finishes at the end of June and then we'll really be able to get started. I have opened the project because basically more and more people were telling me that I had to open it, not because I'm ready to run it! But I will attempt to run it :-)

The rules: if anyone wants to "claim" any of the below tasks, make themselves known on this thread.

I am still getting the hang of the colour scheme on the blueprint graph. Right now ignore border colours of everything. As for interior colours, green means "done", blue means "could well be ready although feel free to ask" and no colour means "unlikely to be ready".

So let's go through the blue nodes.

1) fermatLastTheoremThree: this is FLT for p=3 and it's being worked on by the LFTCM team e.g. @Pietro Monticone . My impression is that it's all under control; the node will go green when the result is in mathlib.

2) FLT.FreyPackage.of_not_FermatLastTheorem: this is elementary but long. The sorrys are in of_not_FermatLastTheorem_coprime_p_ge_5. The goal is "this algorithm which obviously works, works". The algorithm is "given a,b,c a counterexample, cast out divisors and swap them around a bit (possibly changing signs) and you can obviously guarantee that b is even and a is 3 mod 4" and then the goal is to prove that the algorithm works.

3) FLT.FreyCurve: this is filling in the sorries here https://imperialcollegelondon.github.io/FLT/docs/FLT/Basic/Reductions.html#FLT.FreyPackage.FreyCurve . This involves knowing how to compute the discriminant of a plane cubic, perhaps spotting some factorization of a denominator, and basically verifying that the curve I've written down is nonsingular.

4) group_theory_lemma. The work that @David Ang and @Junyan Xu are doing will ultimately show that if A is the abelian group corresponding to the points of an elliptic curve over an alg closed field of char 0, then the n-torsion in A has size $n^2$ for all $n\geq1$. I claim that it follows from this that the $n$-torsion must in fact be $(\Z/n\Z)^2$ and I've abstracted out the lemma which proves this. I haven't even formalised the statement in Lean yet so this is what needs doing for starters, and then the proof might be quite fun/challenging.

5) EllipticCurve.Points.map: This is the claim that if E/k is an elliptic curve, and K,L are k-algebras (and fields) and we have a map between them, then the induced map E(K) -> E(L) is a group homomorphism. The proof should just be "take a look at the gory details of the definition and note that it's defined by ratios of polynomials with coefficients in k". Note that right now there is some sorried data (defining the map itself) (this may or may not be in mathlib already, I didn't look). Once this is done, map_id and map_comp should hopefully be very easy.

I think that most other blue things still need some input on my end before they're viable, but there are five starters.

[David Ang]

4 is already done by @Peiran Wu (who's not subscribed to this stream). 5 is already done a while ago in my local branch.

[Ruben Van de Velde]

Please check my open PRs :)

[Kevin Buzzard]

OK @David Ang can you PR 5 to mathlib? Great to hear about 4! Probably mathlib is also the home for this, as although it's a random lemma in group theory it's used (as far as I can see) to analyse the torsion points of elliptic curves.

[Michael Stoll]

It can be generalized to other exponents than 2; I image one can use the more general version to show the corresponding statement for general abelian varieties (and for the multiplicative group, but this will already exist).

[David Ang]

He has the more general version, I think

[Kevin Buzzard]

Michael Stoll said:

It can be generalized to other exponents than 2; I image one can use the more general version to show the corresponding statement for general abelian varieties (and for the multiplicative group, but this will already exist).

Yes -- I write the more general version in the blueprint.

[David Ang]

Seems like I already made a PR for 5, but I was working on other things since January... I'll come back to this asap

Kevin Buzzard said:

OK David Ang can you PR 5 to mathlib? Great to hear about 4! Probably mathlib is also the home for this, as although it's a random lemma in group theory it's used (as far as I can see) to analyse the torsion points of elliptic curves.

[Notification Bot]

A message was moved from this topic to #FLT > p = 3 case by Patrick Massot.

[Mario Carneiro]

I'd like to work on 2, cleaning up and simplifying the path from no Frey Package to FLT.

[Ruben Van de Velde]

Mario Carneiro said:

I'd like to work on 2, cleaning up and simplifying the path from no Frey Package to FLT.

Already done

[Mario Carneiro]

I know the proof is done, I want to clean it up

[Mario Carneiro]

I'll start from your version in FLT#29

[Mario Carneiro]

^ this now linkifies FYI

[Watson Bernard Ladd]

I have to go learn more lean to contribute, but 3 feels pretty squarely in my wheelhouse mathematically/just a calculation? Depends on how much of the theory of nonsingular we still need/can specialize to hyperelliptic. (That said don't take this as a blocker from tackling it yourself as might take too long)

[Ruben Van de Velde]

3 is done

[Ruben Van de Velde]

1/ under control
2/ PR open
3/ done
4/ done
5/ done

[Ruben Van de Velde]

As far as I can tell, so time for a V2 thread, @Kevin Buzzard :)

[Kalle Kytölä]

Extrapolating from this pace with outstanding tasks, it looks like the completion announcement of the 5-year project is due to appear in a thread called Outstanding Tasks, V1826. :sweat_smile:

[Ruben Van de Velde]

I think we should extrapolate in a different axis and conclude that the project will be done by October and Kevin gets to spend the next five years on a beach

[Kevin Buzzard]

I'm in the process of adding some j-invariant tasks. Another thing we can do is start on Weierstrass P-function and quaternion algebras. I have some time tomorrow to work on this but then I've got a busy Friday. I'm sorry I'm not really able to lead the project properly right now.

[Ruben Van de Velde]

No worries, we're just all excited to get started (and speaking for myself, trying to get some contributions in while I can still understand more than one word in three of the blueprint)

[Kevin Buzzard]

OK so FLT.FreyCurve is green, so now Frey_curve_j is blue and also FLT.FreyPackage.FreyCurve.j_valuation_of_bad_prime (which uses it) is also morally blue (I don't really understand why it's not blue -- if something uses a theorem which isn't proved does that make it not blue?)

[Kevin Buzzard]

They're both relatively straightforward; should I make issues for them or just allow people here to claim them?

[Watson Bernard Ladd]

IMHO it's up to how you want to run the project. Making an issue is free, even for small ones, so I'd get started using that if that's the eventual destination just to keep moving people that way. (I used to do much math. Now I do more CS and manage things via github issues reasonably often)

[Kevin Buzzard]

Right now I'm going to be using my traditional approach of not managing anything at all well and just hoping that things will turn out OK. When running this project is my actual job I will hopefully do a better job of it.

@Peiran Wu I added the group theory lemma as a sorry. Fancy making a PR?

[Ruben Van de Velde]

How sure are you that FreyCurve.j is correct? :)

[Kevin Buzzard]

The algorithm was: I copied the definition from Serre, then set p=37 and then made a Frey curve in pari-gp and checked that the answer was correct, and then attempted to copy the result into Lean. So I have some confidence but not a whole lot. It should be $2^8(C^2-AB)^3/(ABC)^2$ where $A=a^p$ etc.

[Kevin Buzzard]

PARI/GP is free software, covered by the GNU General Public License, and comes
WITHOUT ANY WARRANTY WHATSOEVER.

Type ? for help, \q to quit.
Type ?17 for how to get moral (and possibly technical) support.

parisize = 8000000, primelimit = 500000, nbthreads = 20
? p=37
%1 = 37
? e=ellinit([1,(b^p-1-a^p)/4,0,-a^p*b^p/16,0])
%2 = [1, 1/4*b^37 + (-1/4*a^37 - 1/4), 0, -1/16*a^37*b^37, 0, b^37 - a^37, -1/8*a^37*b^37, 0, -1/256*a^74*b^74, b^74 + a^37*b^37 + a^74, -b^111 - 3/2*a^37*b^74 + 3/2*a^74*b^37 + a^111, 1/256*a^74*b^148 + 1/128*a^111*b^111 + 1/256*a^148*b^74, (256*b^222 + 768*a^37*b^185 + 1536*a^74*b^148 + 1792*a^111*b^111 + 1536*a^148*b^74 + 768*a^185*b^37 + 256*a^222)/(a^74*b^148 + 2*a^111*b^111 + a^148*b^74), Vecsmall([0]), [Vecsmall([128, 0])], [0, 0, 0, 0]]
? e.j
%3 = (256*b^222 + 768*a^37*b^185 + 1536*a^74*b^148 + 1792*a^111*b^111 + 1536*a^148*b^74 + 768*a^185*b^37 + 256*a^222)/(a^74*b^148 + 2*a^111*b^111 + a^148*b^74)
? 2^8*((a^37+b^37)^2-a^37*b^37)^3/a^74/b^74/(a^37+b^37)^2
%4 = (256*b^222 + 768*a^37*b^185 + 1536*a^74*b^148 + 1792*a^111*b^111 + 1536*a^148*b^74 + 768*a^185*b^37 + 256*a^222)/(a^74*b^148 + 2*a^111*b^111 + a^148*b^74)
? %3-%4
%5 = 0

[Ruben Van de Velde]

I got it to the point where I expected ring to finish, but it didn't. I'll stare at the expression for a little longer

[Ruben Van de Velde]

Unless it's just that I forgot to substitute out the c

[Ruben Van de Velde]

The ^ 3 got lost

[Ruben Van de Velde]

FLT#38

[Kevin Buzzard]

Sorry!

[Ruben Van de Velde]

I ran out of time on j_valuation_of_bad_prime, but wip is in FLT#39

[Ruben Van de Velde]

If someone wants to pick it up, go ahead

[Peiran Wu]

Kevin Buzzard said:

Peiran Wu I added the group theory lemma as a sorry. Fancy making a PR?

I will make one this weekend. Some of the defs are Mathlib-worthy, but I'll dump everything in the PR first.

[Kevin Buzzard]

Yeah if we could get it all into FLT then we can think about getting it into mathlib later.

[Ruben Van de Velde]

Ruben Van de Velde said:

If someone wants to pick it up, go ahead

Nearly done here

[Kevin Buzzard]

I've begun a new chapter 5 working towards the definitions of the automorphic forms of interest to us in the modularity lifting theorem. There's a new blue node MatrixRing.isCentralSimple : matrix rings are central simple algebras. Not too hard. See https://github.com/ImperialCollegeLondon/FLT/issues/47 (I am not yet clear about whether I should make an issue for a proof this short).

[Ruben Van de Velde]

Kevin Buzzard said:

I've begun a new chapter 5 working towards the definitions of the automorphic forms of interest to us in the modularity lifting theorem. There's a new blue node MatrixRing.isCentralSimple : matrix rings are central simple algebras. Not too hard. See https://github.com/ImperialCollegeLondon/FLT/issues/47 (I am not yet clear about whether I should make an issue for a proof this short).

Pushed half at FLT#50

[Mario Carneiro]

My proof of (2) is up at FLT#51