Top down/bottom up (was:Finite subgroups of PGL_2(F_p bar))

Stream: FLT

[Ryan Smith]

I noticed at the very bottom of https://imperialcollegelondon.github.io/FLT/blueprint/ch_bestiary.html#a0000000080 there is a request for the classification of the finite subgroups of PGL_2(F_p bar). That caught my eye since it looked like an interesting mini project. What is the precise scope of the requirement?

A bit unrelated but there are relatively few unclaimed tasks on github right now. Generating more of these might be helpful to give people places to start with low(er) hanging fruit?

[Kevin Buzzard]

Right now we are in a bit of a transitional period. People are working on a project whose main goal is to prove that a certain Hecke algebra is Noetherian, but I have been concentrating on a new project which involves building from the top down; see the new chapter https://imperialcollegelondon.github.io/FLT/blueprint/ch_freyreduction.html . In the long term this will result in more unclaimed tasks, however probably one would need to be an expert in the area to help with these tasks; basically now we have got to the point where I need to focus on the technical details of what Wiles and others did, which makes it far less amenable to drive-by contributions. I am giving several talks in the next few weeks so I really need to focus on this.

@Alex Brodbelt what is the status of the classification of finite subgroups of PGL_2(F_p-bar)? Alex was working on it for his undergrad thesis but my guess is that the thesis is now submitted.

Ryan -- If you are looking for something to do at undergrad/MSc level then we need the basics of the Weierstrass P-function up to and including P'^2=4P^3+AP+B and the reason we need it is here.

If you are looking for some cute easy sorries at MSc level then unfortunately the problem is that these take time to prepare and right now I am focussed on something else. Basically, you are observing "if you planned out a big project full of stuff which is at MSc level then more people would be able to join in" and I am saying "yes I agree, but actually what needs to be done next is a bunch of stuff at number theory research level". What I promised to do is to prove FLT modulo things which were known in the 1980s so right now any result which was known in the 1980s is not high priority for formalisation.

[Alex Brodbelt]

Still on it! But would be fun if others want to join in!

[Rado Kirov]

I am generally interested in helping out with the FLT project, because I want to learn more algebraic number theory and I generally find writing lean proofs to be a fun puzzle. However, only undergraduate level stuff is within reach for me right now, so I really appreciate sharing these two problems here and get that this is not a good project for such problems (at least at the moment).

@Alex Brodbelt do you have a canonical reference for your problem? Also any WIP repo to share?

I assume all projects go in two phases:
1) formalize all the definitions and theorem statements, but leave all proofs as sorries
2) fill out all the sorries

I have been doing a lot of sorries through https://github.com/teorth/analysis, but have not done any of 1). I am guessing 1) is much harder (though one might think otherwise) because there are mathematically equivalent ways of defining things that have big implications for writing the proofs. So one has to almost predict how the proofs would work before writing them in order to get do a good job at 1).

How does one learn more on how to get better at 1) especially now that most of undergraduate stuff is already in mathlib.

[Yaël Dillies]

IME your assumption is quite wrong, and steps 1 and 2 are heavily interleaved

[Yaël Dillies]

Learning how to do step 1 is hard. There are plenty of tricks, but the tricks won't bring you all the way. The best way to learn is IMO to try doing it.

[Rado Kirov]

Yeah, that makes sense, it's never waterfall. That makes the problem even harder, as I imagine one needs very deep knowledge in both lean and the math involved to do any part of 1).

At some level I see formalization efforts as turning math into software engineering and in SE generally there is use of interns, new grads, junior folks too. There is a lot of hand-holding, design help, code reviews, etc, but overall I think most experienced folks find the tradeoff worth it. I wonder if the calculus is subtly different here due to the complexity of the math knowledge needed.

[Michael Rothgang]

In my experience (lots of Lean, not number theory) this analogy I'd not wrong. But, to match the analogy: you need a suitable project to give to the intern (and a mentor).

[Michael Rothgang]

My impression above is that FLT right now may not be one.

[Ruben Van de Velde]

I wonder if, in parallel to the top-down work that needs quite some number theory experience, there's room for some bottom-up work that would be useful if we ever want to get to a full formalized proof. Clearly Kevin doesn't have time to build a detailed blueprint for such a project, but maybe with a few pointers to results that are within reach and a standard reference work to follow, other people could work towards that independently

[Alex Brodbelt]

@Rado Kirov I have a blueprint which I need to fix (very likely won't build) and ideally move to verso because I'd love to become well-versed (:wink:) in verso. The main reference I am using right now is a masters student's thesis which is an exposition of the classification of SL(2, F) over alg closed F, very accessible.

[Alex Brodbelt]

ClassificationOfSL

[Kevin Buzzard]

There are an absolute ton of bottom-up things which need doing and which would definitely be suitable projects for people who had the required knowledge; such projects would also be suitable for inclusion in mathlib.

Off the top of my head, some examples:

• Weierstrass P-function
• Unramified extensions of local fields (waiting on #27465)
• Galois cohomology
• Galois cohomology of local fields (see https://imperialcollegelondon.github.io/FLT/blueprint/ch_bestiary.html 13.4 to 13.9 for examples of goals)
• classification of finite subgroups of PGL_2(F_p-bar)
• Riemann-Roch (even the statement would be a big step forward)
• Definition of a reductive algebraic group
• Elliptic curves as schemes and proof that locally they're the same thing as plane cubics
• Modular curves (@Kenny Lau has had some thoughts about this)
• Abelian varieties
• Siegel modular varieties (actually we need certain unitary Shimura surfaces but you have to start somewhere)
• Jacobians of curves over fields
• Etale cohomology (e.g. relation of H^1(curve) to tate module of Jacobian)
• Reduction of elliptic curves (reviews of #28115 welcome)
• Tate curve (needs Weierstrass P, see the mathoverflow question above)

I'm sure that I could double this list's length if I actually thought about it rather than just rattling off some stuff off the top of my head. These are all things which I could imagine being taught at MSc level at a strong university. They were also all known in the 1980s and in fact probably the 1960s or earlier, so they are not high priority for me right now, I am not motivated to write a blueprint but I can certainly tell people more precise statements if they ask.

FLT has been running for a year now and I spent the first third of that time travelling round the world and getting nothing done, and the next two thirds of that time working on bottom-up stuff, but this experience has taught me that working bottom-up will simply take an infinite amount of time, so I have switched to top-down in the last month and will be working hard on top-down for the foreseeable future, making it far harder for drive-by collaborations. I am still highly confident that we will reduce FLT to the 1980s within the next 4 years but only if I aggressively target top-down; bottom-up just takes too long. Take a look at the mountain of stuff we have in FLT on the way to proving some standard result which was known in the 1960s (this finiteness result which I've spent most of this year on). We have generated a bunch of stuff which all should be in mathlib but is still not finished and there's a pile of stuff in FLT/Mathlib which needs PRing but who wants to do that? It's not fun. Right now I just need to spend the next two weeks working top-down because I have talks to give, but after that I will turn back to bottom-up and try and help the two big bottom-up projects (finite-dimensionality of spaces of auto forms, and local CFT) over the line, but then I suspect I will be abandoning bottom-up for a while, simply because it's too time-consuming.

[Ryan Smith]

That is quite the todo list. Just explaining the definition of etale cohomology to lean sounds like a formidable task. On the plus side, the more top down work you do the more work can be farmed out to grad students and community members.

Weierstrass P-function sounds like the lowest hanging fruit for someone who knows (knew?) some math but is still actively wrestling with lean. It looks like mathlib already has the P-function, so it shouldn't be too hard to show P'^2=4P^3+AP+B.

For new contributors to the project how do you handle code reviews? Experienced contributors can just submit a PR but for starting out I imagine there may be whole sections of work which need to be ripped up and redone when new contributors formalize things in ways which will cause problems for the future.

[Rado Kirov]

The main reference I am using right now is a masters student's thesis which is an exposition of the classification of SL(2, F) over alg closed F, very accessible.

Indeed, this seems around the right level for formalization to attempt to contribute for me - has accessible single reference and prerequisites are math known around 1850-1870, to get to math known around early 1900s. If you put the project on github I can try to submit some PRs.

I see the common problem that in order of fun - 'proving stated theorems in Lean' > 'stating theorems in Lean' > 'writing a blueprint in LaTeX on how to state the theorems'. But the project needs to go in the opposite order and is much less parallelizable in the initial steps. And there is the problem of simple statements, that have very complex proofs (like FLT), so only by actually filling out the sorries one connects with the next layers.

Right now I just need to spend the next two weeks working top-down because I have talks to give, but after that I will turn back to bottom-up and try and help the two big bottom-up projects (finite-dimensionality of spaces of auto forms, and local CFT) over the line, but then I suspect I will be abandoning bottom-up for a while, simply because it's too time-consuming.

Thank you for compiling this list! This definitely feels like the right call - the one non-negotiable goal of the project is to produce the top proof of FLT, the bottom is declared somewhat open (math known in 1960) and that's where the project has most flexibility, so it doesn't make sense to fix that part too early. By attempting to start proving the top results, you will be forced to define and state lower level concepts, and can freely use sorries there. While the bottom is more parallelizable in principle, there is a risk that it doesn't "connect" well at the higher levels, or even worse the project never gets to the higher levels beyond the blueprint, because it runs out of time.

Personally, my current number theory knowledge is somewhere in the early 1900s (galois theory, marcus' number fields), which means I can't meaningfully contribute to the project, but that is ok, will keep lurking and eventually the top approach will (in 2-3 years) deliver defined and used in the top layers mathematical statements known around 1950 that still need proofs to fully connect and my knowledge will connect with current set of sorries.

[Ruben Van de Velde]

I imagine Kevin won't be able to spend time on reviewing these projects either, and there's no urgent need to connect them with the top-down work, so they can either go directly into a mathlib branch or into a separate project run by whoever feels like it

[Kevin Buzzard]

Ryan Smith said:

Just explaining the definition of etale cohomology to lean sounds like a formidable task.

On the contrary, I think we have most of the machinery required to do this in mathlib already. The problem would probably be that we'd end up defining it via some fancy derived definition which would end up as being unusable in practice.

[Kim Morrison]

Kevin Buzzard said:

and there's a pile of stuff in FLT/Mathlib which needs PRing but who wants to do that? It's not fun.

There needs to be a plan for this, nevertheless! I wonder if Claude can help. :-)

[Ruben Van de Velde]

Any maintainer could help a tiny bit by merging #29332 :)

[Kim Morrison]

Claude just produced

feat: add piCongrSigmaFiber and piCongrFiberwise equivalences #29706

from the prompt

Please read FLT/Mathlib/Logic/Equiv/Basic.lean, and also the corresponding file in the Mathlib repository. Please prepare a PR to Mathlib containing this content, putting it at an appropriate point in the corresponding Mathlib file. Make sure the PR is label FLT, and write in the PR comment an explanation that the PR was prepared by Claude, including quoting the prompting.

[Kevin Buzzard]

@Salvatore Mercuri this was your work, I believe.

[Salvatore Mercuri]

Kevin Buzzard said:

Salvatore Mercuri this was your work, I believe.

Oh nice, so it was! I can also take a look through the Mathlib folder and PR some stuff I added there