Next steps in the formalization

Stream: FLT

[Stepan Nesterov]

I am trying to get a feel for what needs doing in the project right now. My understanding from reading the blueprint (correct me if I'm wrong, and I'm likely wrong) is that the miniprojects are being actively working upon and close to completion, and the next immediate steps could be:

• Deducing FLT.Mazur_Frey from Mazur's torsion theorem (written up by Serre in 1989, apparently known to Frey a few years earlier but unpublished, so technically known in the 1980's, but barely so)
• Formalising the definition of hardly ramified representations and proving that the residual representation of the Frey curve is hardly ramified (same)
• Formalising the statements of results in appendix 13, which are needed to formalise the definition of automorphic form on GL_n/general G (doesn't the project only need automorphic forms on D^x, D totally definite quaternion algebra?)
  For people with required PhD-level knowledge, which directions seem more important to try to work on?

[Kevin Buzzard]

Right now the situation, as I understand it, is the following.

a) There are several "miniprojects" comprising some of the later chapters in the blueprint: for example adeles, Haar characters, finite-dimensionality of quaternionic modular forms. All of these projects are partially done, I think every issue I created got claimed, I've had a busy summer and feel like I don't know what's going here. These became low priority for me because other people were doing them and they were known in the 80s (indeed the 60s). However they do lead to a very nice result -- finite-dimensionality of quaternionic modular forms and Noetherianness of a Hecke algebra, both of which are essential and also interesting (classical modular forms are known to be finite-dimensional in Isabelle and apparently we're close in Lean, but this result is finite-dimensionality of a far more exotic space of automorphic forms)

b) I have decided to make inroads from the top. I have defined hardly ramified Galois representations here and I'm working on stating the four main theorems about them (p-torsion in the Frey curve is hardly ramified, mod p hardly ramified irred Galois rep lifts to p-adic hardly ramified, hardly ramified p-adic spreads out to compatible ell-adic family, and 3-adic semisimple hardly ramified rep is 1+cyclo). This is technical stuff and I felt it unlikely that randomers would be able to help so I've just been doing it myself.

c) I've also been concentrating on stating other hard theorems and definitions, e.g. cyclic base change in the form I want it, modularity of Galois reps, modularity lifting theorem which I want etc. Again it's difficult to see how others can help here, I've been working with Andrew Yang.

d) I've also been working on the class field theory repo because I think we'll need the local Artin map and we almost have a definition. This is a project which we've been working on privately with the people who came to the Oxford class field theory workshop.

I was not going to prove that E semistable and Mazur and p>=5 and E[2] trivial implied E[p] irreducible; this needs an argument involving things like isogenies of elliptic curves and more, all of which was known in the 80s but not known to Lean, so this looks like a biggish project but as I say it was known in the 80s and right now I am simply sorrying everything known in the 80s. Same for Frey[p] hardly ramified (this needs the theory of the Tate curve, which needs the Weierstrass P-function, all needs doing to finish the job, all known in the 80s so I was not personally concentrating on it).

As for auto forms on GL_n or general G, I have convinced myself that the only definition I need is for a tot def quat alg over a tot real field and then I can just invoke stuff like Jacquet-Langlands which was known in the 80s and not even define e.g. Hilbert modular forms.

One project which is coming up is that a 3-adic semisimple hardly ramified Galois rep is 1+cyclo. I don't know a pre-1990 reference for this so it needs doing. The proof is: first show that a mod 3 hardly ramified Galois rep is (cyclo *;0 1) using the same sort of argument as in Fontaine's abelian schemes paper and Odlyzko bounds (I think in this case actually due to Poitou) and then some devissage (I didn't type up the LaTeX yet). Again one wouldn't have to prove the Fontaine or Poitou results as these were known in the 80s, and everything else is straightforward. This seems to me like a reasonable project although you'll have to know some Lean as well as the maths (or ask lots of questions) and I can prioritise the LaTeX write-up if you want to take it on but I am not sure how much Lean you know or if indeed you're actually looking for a project as opposed to just asking where we are.

[Stepan Nesterov]

So basically the case p=2, l=3 of Schoof’s paper ‘Semi-stable abelian varieties over Q with bad reduction in one prime only’? (just the finite flat group schemes part, because Lean doesn’t know and doesn’t need to know abelian varieties) (That’s 2005, but just to confirm that this is what you have in mind)
My experience with Lean is limited, I just worked my way through mathematics in Lean. But in terms of math, I think I know the argument well enough (and it’s in my RAM because Stanford’s Student Algebraic Geometry Seminar I’m co-organizing in on this exact topic this quarter) that I would be open to just formalizing the statements directly from research literature in Lean and try to learn more Lean this way.
But if that’s not the project you would trust a relative novice at Lean with, that’s totally fine, I’ll just continue cheering from the sidelines and wait till something more accessible comes up :)

[Kevin Buzzard]

If you're at Stanford -- it was the argument Taylor presented in his course in Jan. I can prioritise writing up the argument but if you went to the course or know Dongryul Kim and ask them for their notes then it's the stuff in lectures 4 and 5. Of course you can also ask Jared to get math.inc to do it ;-) but I don't know if their system is up to it yet (time will tell).

[Stepan Nesterov]

From what Jared told us in his talk, it took him 2-3 weeks to formalize the trivial N^(2/3) de Brujin bound with Lean, and agent was making a lot of mistakes just as you would expect from an AI agent

[Stepan Nesterov]

And that was elementary analytic number theory we’re talking about, not Galois representations and finite flat group schemes

[Stepan Nesterov]

But anyway, given that I know what the argument is mathematically, and I’m willing to try and write up some Lean, what’s the process here? Formalise the statements of all the sublemmas first, and get some feedback from the more lean-savvy people if that looks ok?

[Stepan Nesterov]

Or is it more reasonable for me to just wait for the blueprint, if you’re planning to write it anyway?

[Kevin Buzzard]

If you're a beginner then formalising statements is hard; it's much easier to formalise proofs. You're taking on a bit of a ridiculous project for a first project, I spent weeks doing things like proving sqrt(2) was irrational before tackling serious mathematics, but who knows. You definitely learn by doing projects. Why don't you read some Mathematics In Lean and wait for me to do some of the theorem-stating?

[Stepan Nesterov]

Ok :+1:

[Stepan Nesterov]

I could also try to tackle something like Appendix 13.2 or classification of finite subgroups of PSL(2,Fp bar), which are much easier mathematically.
It just seems like from what you're saying now they don't really need doing because they were known in the 80s

[Stepan Nesterov]

Actualy the latter one was known in the 1880s most likely

[Kevin Buzzard]

If you want to do some of the mathematics yourself, here is something which I haven't got clear in my head yet. Let's assume that if K/Q_3 is finite with integers R and max ideal m and if rho:Gal(Q-bar/Q)->GL_2(R) is hardly-ramified (I linked to the definition above), then rhobar:Gal(Q-bar/Q)->GL_2(R/m) is hardly ramified. Let's also assume that if rho as above is hardly ramified and if we conjugate rho by some matrix in GL_2(K) and the result still lands in GL_2(R) then this conjugate is also hardly ramified; these should not be hard to prove modulo theorems from the 1980s. Finally let's assume that if rhobar:GQ->GL_2(k) is hardly ramified with k a finite field of characteristic 3 then rhobar is an extension of trivial by mod 3 cyclo. By choosing various lattices carefully, one should be able to deduce that rho tensor K to GL_2(K), semisimplified, is trivial + cyclo. Can you write down a careful mathematical proof of this?

[Stepan Nesterov]

Yea sure

[Stepan Nesterov]

Richard used a Zorn's lemma argument in this one which is pretty funny

[Kevin Buzzard]

He also twisted by cyclo because he likes the F-L normalisation better so nothing is flat and all the dets are cyclo^{-1}. In the Shimura variety context there is a good argument for this but in this context I don't really see the point so I'm sticking with the Tate module normalisation

[David Michael Roberts]

Ah, the canonical normalisations, right? ;-)

[Rado Kirov]

I could also try to tackle something like Appendix 13.2 or classification of finite subgroups of PSL(2,Fp bar), which are much easier mathematically.

@Alex Brodbelt and I are hacking away at it on https://github.com/AlexBrodbelt/ClassificationOfFiniteSubgroupsOfPGL

It is indeed easy enough mathematically that I can follow the math, but still 50 pages of non-trivial group theory (based on https://lup.lub.lu.se/luur/download?func=downloadFile&recordOId=8998907&fileOId=8998908), so quite a bit of Lean work required.

I am interesting in joining a working group on some subtasks here. Both my math and Lean are currently lacking, but hoping to pick up Lean faster, and can come down to Stanford once a week (I am based in SF).

[Kevin Buzzard]

Because there is no blueprint and the work I need doing is technical (we can skip everything known in the 80s and need to engage with the difficult stuff in the Wiles paper) it's hard for me to find natural stuff to pass off to other people. One of the things on my job list in October is to take stock of the mini projects and find out what's going on

[Alex Brodbelt]

Stepan Nesterov said:

I could also try to tackle something like Appendix 13.2 or classification of finite subgroups of PSL(2,Fp bar), which are much easier mathematically.
It just seems like from what you're saying now they don't really need doing because they were known in the 80s

If you want to help formalizing this, there are definitely suitable tasks/lemmas for you if you are not as familiar with Lean. DM me or Rado if you would like more details (: .

[Notification Bot]

29 messages were moved from this topic to #FLT > Hardly ramified representations by Kevin Buzzard.