Oooh, thanks. I've been thinking a bit about formalizing n=3 or n=4 in
metamath (or perhaps more likely, encouraging others to do so) but I was
just thinking in terms of something we could accomplish soon, I didn't
realize that the proof via the Modularity Theorem also needed those
cases to be proved separately.
I've taken the liberty of writing up what has been posted in this thread
so far at https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theorem
which is part of the metamath wiki - I did so with the intention that
other people could edit as we learn new things (I'm not sure I know the
github permission system to know who already has an "edit" button but if
anyone doesn't, just post proposed changes here or to a github issue or
whatever).
On 2/20/23 04:42, David Crisp wrote:
(Breaking my years-long lurking habit to post this :))
One thing that's often left out in discussions of how to formalize FLT
is that even if the entire Frey - Serre - Ribet - Wiles sequence is
included, the cases n=3 and n=4 will still need to be added as
separate proofs. It's not obvious from a 'casual' read of Wiles'
paper, but the level-lowering procedure used by Serre and Ribet to
establish the non-modularity of the Frey curve is only guaranteed to
work if the exponent in the Fermat equation is an odd prime != 3.
Induction over the multiplicative structure of N then establishes the
theorem for all n except those whose only prime factors are 2 and 3,
but the n=3 and n=4 cases would still need to be proved separately to
complete the proof.
Luckily these two cases are fairly elementary to prove individually
(especially compared to the monumental task of formalizing the entire
modularity theorem) and so are often handwaved away in informal
discussions, but a formal system like Metamath obviously can't do that.
Dave
On Sunday, 19 February 2023 at 04:05:37 UTC [email protected] wrote:
Looks like
http://www.ipam.ucla.edu/abstract/?tid=19347&pcode=MAP2023
<http://www.ipam.ucla.edu/abstract/?tid=19347&pcode=MAP2023> has
both an abstract (which goes into more detail about what the talk
is about) and a video of the talk.
Maybe you'd be able to figure out where this fits into your
outline; I'm afraid I'm even less far up the learning curve than you.
On February 18, 2023 7:58:11 PM MST, Steven Nguyen
<[email protected]> wrote:
I've actually taken some notes over Fermat's Last Theorem:
https://docs.google.com/document/d/19dXkojJJt6gq9rYLo6zbz7HpHpD9iMJJkY0LEpGqPs0/edit?usp=sharing
Although so far, all that has come out of it are some useful
resources, definitions, and the overall structure of Fermat's
Last Theorem, which I summarize here:
1.
Modularity Theorem (previously the Taniyama-Shigura(-Weil)
conjecture): every rational elliptic curve is modular
2.
Yves Hellegouarch came up with the idea of associating
hypothetical solutions (a, b, c) with elliptic curves of
the form y^2 = x(x − a^n)(x + b^n).
1.
Such curves are called Frey curves or
Frey-Hellegouarch curves.
3.
Ribet’s Theorem (previously called the epsilon or
ε-conjecture): All Frey curves are not modular
Note that the final paper by Wiles proved a special case of
the modularity theorem for semistable curves over ℚ. In this
case, "Frey curves are semistable" would have to be proved as
well.
This is enough to prove FLT. If there were any solutions, then
there would be a corresponding Frey curve. By Ribet’s Theorem,
the curve would not be modular, but that contradicts the
Modularity Theorem. Therefore there are no fermat triples, FLT
is proved. ∎
However, I admit I don't understand almost all of the theory
behind FLT... I've never heard of local field class theory. So
that's quite an interesting link.
On Thursday, February 16, 2023 at 8:36:10 PM UTC-6
[email protected] wrote:
I know this is a bit of a white whale and there is a lot
of mathematics to formalize before this is even in reach.
But when the formal math community (taken as a whole) is
at 99 out of 100 of the Top 100 list, of course it is easy
to focus on the one.
Anyway the news is that there was a recent talk on
formalizing local field class theory which apparently is
one of the things that will be needed.
https://mathstodon.xyz/@tao/109877480759530521
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/308508e3-2ad5-41ae-b362-1c7aa5983207n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/308508e3-2ad5-41ae-b362-1c7aa5983207n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/91add638-5d2d-640c-4314-9c104e205916%40panix.com.
