FLT-regular

Stream: Lean Together 2024

[Riccardo Brasca]

Concerning Kevin's questions about FLT5, here I've started the proof.

There are three sorry in the file:

• the first one is a boring but easy one: just check that the coercion from ℤ to ℚ of (-1)^(...) is what it should be.
• the second one is the inequality 125 < (2 * (π ^ 2 / 16) * (32 / 3)) ^ 2. It shouldn't be difficult (it is enough that 3 < π).
• the third one is the fact that the number of complex places of the 5th cyclotomic field is 2. This shouldn't be very difficult but we need to work a little bit on it.

[Riccardo Brasca]

Thanks gcongr, the inequality was really easy.

[Riccardo Brasca]

And I don't know how but simp did the first one :D

[Andrew Yang]

We should show that cyclotomic fields are totally complex and then use docs#NumberField.InfinitePlace.card_eq_card_isUnramifiedIn

[Johan Commelin]

So only the 3rd sorry remains?

[Riccardo Brasca]

Yes, I am working on it, it's also rather easy

[Riccardo Brasca]

It's done. It should be golfed and generalized, but it wasn't very difficult.

[Kevin Buzzard]

The reason I'm specifically interested in 5 is that this is a curve of huge genus (6 I guess?) with lots of local points (and a few global ones), and so finding all rational points on it is a really nontrivial achievement. The n=4 case $x^4+1=z^4$ (dividing through by $y$) has genus 3 but it maps onto a rank 0 genus 1 curve $x^4+1=Z^2$ so it's still easy -- methods known to Fermat will (and did) do it. I conjecture that such a high genus Diophantine equation has never been explicitly solved in any other prover -- this is genuinely hard in some sense.

[Michael Stoll]

In fact, the $p = 5$ case of FLT reduces to rational points on a genus 2 curve. Generally, for $p$ an odd prime, FLT holds for $p$ iff the (hyper)elliptic curve $y^2 = x^p + 1/4$ has only the obvious rational points. In the $p = 5$ case, one can easily (not in Lean, but in Magma) compute that the 2-Selmer group is trivial, from which it is easy to conclude.

[Michael Stoll]

(I actually have a proof of FLT(37) that "only" relies on GRH for the computation of the class group of $\mathbb{Q}(\sqrt[37]{2})$.)

[Michael Stoll]

(The paper is here.)

[Kevin Buzzard]

So we can push through this proof once you've finished formalising your Acta Arith paper on 2-descent for Jacobians of hyperelliptic curves :-)

[Kevin Buzzard]

Is the class group of $\mathbb{Q}(2^{1/37})$ not provably computable without GRH?

[Michael Stoll]

It is in theory :smile: . One could try to let the computation run for a while; it may be feasible unconditionally. The input needed is that the class number is odd. (Experimentally, all these fields have class number 1, but of course nothing general can be proved...)

[Michael Stoll]

Kevin Buzzard said:

So we can push through this proof once you've finished formalising your Acta Arith paper on 2-descent for Jacobians of hyperelliptic curves :-)

Possibly. We'd need to have Jacobians and Selmer groups first, so right now, this is some way off (but certainly on my radar).

[Chris Birkbeck]

Kevin Buzzard said:

Is the class group of $\mathbb{Q}(2^{1/37})$ not provably computable without GRH?

The Minkowski bound is 2715982925229018753717, which makes me think no.

[Kevin Buzzard]

Selmer groups we're working on at Imperial. Jacobians I am very unclear about how to do them.