Form. of class num. comp. & Mordell eqns - NIrvana Coppola

Stream: Lean Together 2024

[Mario Carneiro]

Is Siegel's theorem (some class of elliptic curve equations have finitely many integer/rational solutions) or any special cases of it formalized in lean?

[Alex J. Best]

No, only the examples in the paper. Though the techniques would be not so far away from doing a finiteness proof in general (at least for mordell curves) we didn't do that

[Kevin Buzzard]

The finiteness result is quite "deep" in some sense. Mario -- the theorem is that all elliptic curves only have finitely many integer points, e.g. only finitely many integer solutions to $y^2=x^3+Ax+B$ if $A,B\in\Z$ and $4A^3+27B^2\not=0$ (i.e. the cubic has distinct roots in $\mathbb{C}$). You need this hypothesis, e.g. $y^2=x^3$ has infinitely many integer solutions $y=t^3,x=t^2$.

[Mario Carneiro]

Right, I was wondering if for some particular elliptic curves it's easier (or if this theorem is a dependency and was formalized already)

[Chris Birkbeck]

Alex J. Best said:

No, only the examples in the paper. Though the techniques would be not so far away from doing a finiteness proof in general (at least for mordell curves) we didn't do that

You could formalise this fun exercise with what you have done, without too much work, as it doesn't require you to compute any class numbers.

image.png

[Chris Birkbeck]

Or maybe you already did it and I just missed it

[Michael Stoll]

Counterexamples when the class number is not divisible by 3 (in Magma):

> [d : d in [-100..-1] | d mod 4 in {2,3} and IsDivisibleBy(ClassNumber(4*d), \
3)];
[ -89, -81, -61, -54, -53, -50, -38, -29, -26 ]
> [IntegralPoints(EllipticCurve([0, d])) : d in $1];
[
    [ (5 : 6 : 1) ],
    [ (13 : -46 : 1) ],
    [ (5 : -8 : 1) ],
    [ (7 : 17 : 1) ],
    [ (9 : 26 : 1), (29 : 156 : 1) ],
    [],
    [],
    [],
    [ (3 : 1 : 1), (35 : -207 : 1) ]
]

[Kevin Buzzard]

this theorem is easier but it's also explicit; Siegel's result was not explicit, it's an abstract "finitely many solutions" result. I guess Baker's results make it explicit but historically this was later; some result is known of the form $|x|,|y|<10^{10^{10^{10^{max |A|,|B|}}}}$

[Mario Carneiro]

@Kevin Buzzard Would you expect the finiteness theorem to be a dependency of FLT?

[Eric Wieser]

A question for the community: is it time to merge some subset of docs#ZSqrtd and docs#Complex and docs#GaussianInt and docs#Unitization and docs#TrivSqZeroExt into a single structure that would work here too for $\mathbb{Q}[\sqrt{d}]$?

[Anne Baanen]

@Patrick Massot (Can't speak right now, sorry!) The reason we have d : ℤ and d' : ℚ in the statement is that for applying we want to specify the rational number, but the hypotheses require integers. (Specifically, we can't say d' % 3 = 2.)

[Anne Baanen]

Rewriting across the equality ℚ(√6) = ℚ(√(↑6)) would be very annoying.

[Patrick Massot]

This rewriting is what I had in mind. Why is it annoying?

[Nirvana Coppola]

https://github.com/lean-forward/class-group-and-mordell-equation

[Kevin Buzzard]

I don't think that either Siegel's result or the (much harder) theorem of Faltings saying that for genus > 1 (e.g. y^2=quintic with 5 distinct roots)) there are only finitely many rational solutions will be needed for FLT.

[Anne Baanen]

We'd have to transport the variables, equalities and the field structure, and the result is there are lots of casts in the resulting statement. It would in the end all be hidden behind the API surface but the same is true of the current "double d" approach.

[Anne Baanen]

It's been a while though, let me see if I can recover an explicit example.

[Alex J. Best]

It was because we used specific numbers at some point and want to work with QuadRing rat 0 (-2) and not QuadRing rat 0 ↑(-2)

[Alex J. Best]

This might work out differently with lean 4 numerals, but I'm not convinced that we wouldn't still want something like that

[Anne Baanen]

There also was a question about norm_num exensions: in fact we implemented our prototype times table tactic as a norm_num extension. Mathlib 4's norm_num forces the output of the tactic to be a (rational) numeral so the Lean 4 port instead extends ring. The Lean 4 port of the times table tactic works but needs to be optimized to make it really useable. That's one of the things I have been spending my (very limited!) research time on.

[Mario Carneiro]

I think this is fixed now?

[Mario Carneiro]

Or maybe that PR never landed...

[Anne Baanen]

Mario Carneiro said:

I think this is fixed now?

Sorry, what are you referring to here?

[Mario Carneiro]

the fact that norm_num does not allow other types

[Mario Carneiro]

#8100

[Anne Baanen]

AFAICT, docs#Mathlib.Meta.NormNum.Result' still doesn't allow returning an expression of the form 1 + 2 √ 5.

[Junyan Xu]

Eric Wieser said:

A question for the community: is it time to merge some subset of docs#ZSqrtd and docs#Complex and docs#GaussianInt and docs#Unitization and docs#TrivSqZeroExt into a single structure that would work here too for $\mathbb{Q}[\sqrt{d}]$?

Here's some Lean 3 code defining adjoin_root as a vector with computable multiplication.

[Anne Baanen]

Anne Baanen said:

It's been a while though, let me see if I can recover an explicit example.

I tried restating Mordell_d' with casts and the result consisted of timeouts at each point we try to apply it to a concrete value of d. So maybe in simpler proofs unification can work but here it fails.

[Kevin Buzzard]

I guess lean 4 completely changed how numerals work so it might be worth looking at this again after porting?