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/1ceff94e-aa1a-411f-bb69-8dea80fd6a59n%40googlegroups.com.
