Zulip Chat Archive

There seems to be a lot done in elliptic curves in Isabelle and Coq because it is useful for cryptography, so funding comes from entities interested in cryptography applications.

Kyle Miller (May 20 2023 at 01:04):

@Lars Ericson I'm not sure I really understand what thesis you're trying to support regarding FLT. I'm inferring that you're hoping to get people interested in working on formalizing FLT itself, and that you're trying to be a problem solver and eliminate what you yourself are perceiving to be impediments toward this work.

Have you had a chance to look at mathlib yet? This is the main project we're working on, which is an attempt to formalize all basic undergraduate and research mathematics in a single library. There's a lot of math to do, and not having FLT yet does not mean that work isn't progressing ever-so-incrementally toward such targets. As that first link you shared says, "On the other hand, I do think that the challenge [to formalize FLT] is doable, and that it will be done in the coming fifty years. It is definitely not within reach. The project will have to cover large parts of current pure mathematics. Its scope is comparable with the Bourbaki project, where between 1950 and 1970 almost all of pure mathematics got a new foundation." Mathlib is quite young.

There's an ongoing project to prove FLT in the case of regular primes: https://github.com/leanprover-community/flt-regular

Lars Ericson (May 20 2023 at 12:13):

@Kyle Miller my own sense of easy-to-hard-part is:

Define the structures like elliptic curve and modular form that the Wiles proof talks about
State the top-level flow with sorrys of the main proof
Finish the proof on initial parts of the proof if these have already been done
Separate out the hard parts and frame these as separate subgoals

I'm looking at the past efforts in this regard, in Lean and related ancestors of Lean like Coq and Isabelle. For reasons I don't understand, Lean seems to have an open community which is 100x larger and 100x more active than the Coq/Isabelle communities. Historically I don't know why this is the case. But it definitely seems like Lean is where it's at.

I know that these steps are, from an expert's point of view, uncomfortably trivial. I don't really agree. I think it is useful work to have the language available to state the top level of the proof, which looks easy, because the statement of FLT is something that anyone can grasp, because that makes it easier to frame the hard parts on their own terms, which will be terms that only specialists can grasp, which makes it easier for people like me who are non-specialists to say "Oh right, that does look hard" and walk away. So a statement like "A remarkable elliptic curve cannot be modular" is clearly cognitively far enough away from "there is no $n>2$ such that $x^n+y^n=z^n$ " that I can look at it and say "oh that does look hard and I don't understand it and I don't want to understand it but it's good that someone else is thinking about it".

There is another moving part though which is the redesign of Lean 3 to Lean 4. Google Bard told me I should work in Lean 4:

Screenshot-from-2023-05-20-08-07-02.png

So in that regard I have done scripts/start_port.sh Mathlib/RingTheory/PowerSeries/Basic.lean and I will focus on that. If I can't make that file typecheck on my PC, I will promptly give up on the larger outline above. I don't expect anybody else to follow that approach, it just seems like the right path to me.

Lars Ericson (May 20 2023 at 12:49):

Regarding the project to prove FLT for regular primes, that leaves the subgoal of proving it for irregular primes. @Kevin Buzzard commented here that "Wiles' proof does not distinguish between the regular and irregular case. He proves semistable Taniyama-Shiumura, which doesn't have a prime in its statement." This is exactly why I think we should state the top-level flow of the version of Wile's proof that we really want to end up at. That is, either you commit to a proof which does regular and then irregular primes, which is different from Wile's proof, or start at least with a top-level outline which you think is achievable and correct of what you think Wile's proof does in a flow that Wile likes.