Mordell's theorem

Stream: Is there code for X?

[Ryan Smith]

Has Mordell's theorem been formalized in lean? The amount of information about elliptic curves in mathlib was smaller than I expected. Even better would be Mordell-Weil but I'm going to guess that's a no?

[Bryan Wang]

Regarding Mordell-Weil, I'm looking to (define and) formalize some basic facts about abelian varieties, and I'd be even happier if anyone is also interested to work together on this!

[Ryan Smith]

Right now I feel like I'm wrestling with an anaconda trying to formalize Burnside's theorem while still being very new to lean. By the time I finish maybe I'll be good enough with lean to be useful.

[Scott Carnahan]

Even a proof of the fact that a proper fiberwise-connected group scheme is commutative would be an interesting test of the algebraic geometry API.

[Bryan Wang]

Scott Carnahan said:

Even a proof of the fact that a proper fiberwise-connected group scheme is commutative would be an interesting test of the algebraic geometry API.

Yep, that would be what I'm (hoping to) work towards.

[David Ang]

Ryan Smith said:

Has Mordell's theorem been formalized in lean? The amount of information about elliptic curves in mathlib was smaller than I expected. Even better would be Mordell-Weil but I'm going to guess that's a no?

No - I had a go at it a few years ago in some branches in mathlib3 but it has not been ported over

[David Ang]

Back then the issue was that we didn't have Galois cohomology and a good local theory (which I guess we still don't), and I only did heights over Q

[Bryan Wang]

David Ang said:

Ryan Smith said:

Has Mordell's theorem been formalized in lean? The amount of information about elliptic curves in mathlib was smaller than I expected. Even better would be Mordell-Weil but I'm going to guess that's a no?

No - I had a go at it a few years ago in some branches in mathlib3 but it has not been ported over

This is based on the Weierstrass curve definition of elliptic curves?

[David Ang]

I do have intentions to continue doing this once I finish writing my thesis this month.

[David Ang]

Bryan Wang said:

David Ang said:

Ryan Smith said:

Has Mordell's theorem been formalized in lean? The amount of information about elliptic curves in mathlib was smaller than I expected. Even better would be Mordell-Weil but I'm going to guess that's a no?

No - I had a go at it a few years ago in some branches in mathlib3 but it has not been ported over

This is based on the Weierstrass curve definition of elliptic curves?

Yeah, unfortunately!

[David Ang]

It's here: https://github.com/leanprover-community/mathlib3/blob/mordell_weil/src/algebraic_geometry/EllipticCurve/mordell_weil.lean

(back then we don't even have the group law :P)

[David Ang]

The code was very badly written (given that this was my first Lean project), and I wouldn't go for complete 2-descent if I were to do it again

[Bryan Wang]

David Ang said:

Bryan Wang said:

David Ang said:

Ryan Smith said:

Has Mordell's theorem been formalized in lean? The amount of information about elliptic curves in mathlib was smaller than I expected. Even better would be Mordell-Weil but I'm going to guess that's a no?

No - I had a go at it a few years ago in some branches in mathlib3 but it has not been ported over

This is based on the Weierstrass curve definition of elliptic curves?

Yeah, unfortunately!

Well, it's great that we can talk about Mordell using just the "basic" Weierstrass machinery!

[David Ang]

Yeah, obviously we'll eventually connect it with abelian varieties but I think a lot can be done just with the basic machinery e.g. following Silverman

[Kevin Buzzard]

Just to be clear -- I don't know what "Mordell's theorem" means but finiteness of rational points on curves of genus >= 2 is currently a fantasy. Mordell-Weil is certainly accessible for plane cubics over number fields but has never been done. We don't even have the definition of an abelian variety so Mordell-Weil is not the question here, what we want there is basic stuff like the theorem of the cube or whatever. The big issue with the definition of abelian variety is that there are plenty of definitions which one could choose, all of which are equivalent, but proving equivalence is hard, so there is a big design decision to be made before we even start.

[Michael Stoll]

I think "Mordell's Theorem" refers to the statement that the group of rational points on an elliptic curve over $\mathbb Q$ is finitely generated (what Mordell proved in his famous 1922 paper; I've heard that he did not like his theorem being subsumed under the heading "Mordell-Weil" :slight_smile:).

[Kevin Buzzard]

Oh I see; Mordell-Weil is ab vars over number fields, Mordell is elliptic curves over Q? Did Mordell also assume existence of one or more 2-torsion points? The general plane cubic proof is no harder for number fields than for Q, right?

[Michael Stoll]

As far as I know, Mordell did prove the general statement over $\mathbb Q$. (His 1922 paper does not seem to be available online, which reminds me that I wanted to ask my son, who is in Cambridge, to dig it up for me...)

[Kevin Buzzard]

Cassels taught me a proof of Mordell's theorem when there's a 2-torsion point which goes via two mu_2-descents and is completely elementary because the Selmer group lives in $\mathbb{Q}^\times/(\mathbb{Q}^\times)^2$ so you can do the whole thing without cohomology or class groups/unit groups. He wrote the proof in his little blue book (I went to the lectures which became that book). But if you don't have any 2-torsion then you either do descent on the full multiplication by 2 map (which needs group cohomology, which I suspect he didn't have, although H^1 you can do in a low-level way) or you adjoin a root (in which case working over $\mathbb{Q}$ doesn't buy you anything).

[Michael Stoll]

You can also use the theory of binary cubic and quartic forms, which may do more to restrict you to the rationals. (You need to show that the Selmer group elements are represented by integral binary quartics with bounded invariants, and you need to know that there are only finitely many of these up to equivalence. This is how Cremona's mwrank program works.)

[Kevin Buzzard]

Ryan Smith said:

Right now I feel like I'm wrestling with an anaconda trying to formalize Burnside's theorem while still being very new to lean. By the time I finish maybe I'll be good enough with lean to be useful.

This is many people's experience when learning Lean. My first projects were (standard intro to proof stuff about e.g. sqrt(2), equivalence relations) -> (definition of scheme) -> (definition of a perfectoid space) and the upward curve in the mathematics was possible because of the corresponding upward curve in my ability to use the software which I was picking up along the way as I constantly asked questions on the Lean chat. Basically if you know the mathematics well and are happy to keep asking questions then you can go anywhere, although it might take some time.

[Kevin Buzzard]

Other things we don't have about elliptic curves (which I need for FLT): the Weil pairing (I need det of Tate module is cyclo char), basic reduction theory (I need Tate module is unram at good primes and p-torsion is flat at p if curve has good reduction), Weierstrass P-function (I need Tate curve for plane cubics over p-adic fields, and the usual approach goes via P'^2=4P^3+AP+B, see https://mathoverflow.net/questions/469021/low-level-proof-of-identity-related-to-weierstrass-p-function although the sensible approach is just to do P-function rather than avoid it, as I was suggesting in that question). In case you were looking for things to do ;-)

[Ryan Smith]

Actually I am looking for ways to help with FLT when I finish my first big self-assigned result in order to learn lean. It's going to be a while, right now I'm still trying to get a nonzero vector v \in V in order to prove that 1 is in fact an eigenvalue of the identity map ;) It's surprisingly hard to explain a lot of things to lean, but lemmas from two weeks ago no longer seem so bad so hopefully we're making progress.

[Kevin Buzzard]

If you need help on basic stuff then feel free to post a #mwe and ask in #new members , that's what it's there for.

[Oisin McGuinness]

An online version of the Mordell paper is linked from the references of the Wikipedia article about the Mordell Weil theorem

The link https://archive.org/details/proceedingscambr21camb/page/178/mode/2up?view=theater gives a scan of the whole volume containing the paper; pages "179-192" are what is wanted. (To extract as PDF use the left menu for downloadable files, select PDF, then just export pages 193-206 of the whole PDF.)

Enjoy!

[Ryan Smith]

Kevin Buzzard said:

If you need help on basic stuff then feel free to post a #mwe and ask in #new members , that's what it's there for.

I already fear I spam them a lot, there are some very patient people in New Members answering questions.

For the elliptic curve results you're looking for, is most of that in Silverman or are you thinking of other texts?

[Rado Kirov]

I am interested in joining formalization projects in algebraic number theory. My math is shaky - I have a PhD in an adjacent field (error-correcting codes from function fields), but I left academia ~ 15 years ago, so forgotten most of the little I knew. However, I have been learning lean since beginning of the year and have been making good progress working through Tao's Real Analysis I (~40% done with the ~2000 sorries). I work as a software engineer, so can help with generic software tasks, but haven't explored internals of Lean as a programming language, writing tactics etc.

Feel free to reach out directly, though #new members will give you better chance of reaching more knowledgable folks.

[Bryan Wang]

Ryan Smith said:

Kevin Buzzard said:

If you need help on basic stuff then feel free to post a #mwe and ask in #new members , that's what it's there for.

I already fear I spam them a lot, there are some very patient people in New Members answering questions.

I would just like to say that as a fellow relative newcomer to Lean, I initially had similar apprehension about asking questions, but that the community here on Zulip has been far more welcoming and helpful than I think anyone could ever hope for, and I am very grateful for that :slight_smile:

[Kevin Buzzard]

Nobody is obliged to reply to messages in #new members and indeed plenty of people are not even subscribed to that channel. I have an algorithm: I tend to not respond to people who are using a pseudonym and I don't look at the channel when I'm busy, but if I'm not busy and the question is clearly in good faith by someone wanting to learn, and if I know the answer, then why not answer? This is how I learnt Lean myself (and back then the community only had 20 or so regulars in it!) and I won't forget that. Now there are many many people answering questions there so it's not like you're sucking up one person's time. Ask as many beginner questions as you like there!

[Snir Broshi]

Regarding Burnside's theorem that was mentioned, maybe this will help a little- https://github.com/wupr/order-p-q

[Michael Stoll]

Oisin McGuinness said:

https://en.wikipedia.org/wiki/Mordell%E2%80%93Weil_theorem

The link https://archive.org/details/proceedingscambr21camb/page/178/mode/2up?view=theater gives a scan of the whole volume containing the paper; pages "179-192" are what is wanted.

@Oisin McGuinness thanks!

[Antoine Chambert-Loir]

That's a wonderful paper, it has a nice rewriting by Mordell himself in his book on Diophantine equations.

[Antoine Chambert-Loir]

But that proof is limited to the ground field Q. To get the mordell weil theorem for elliptic curves over number fields, one needs the language of Galois cohomology.

[Antoine Chambert-Loir]

(About this paper, look at the conjectures at the end!)

[Kevin Buzzard]

I confused Mordell's theorem and Mordell's conjecture earlier in the thread, but at least I now know that they were both from the same paper :-)

[Antoine Chambert-Loir]

Yes, as well as the now called Siegel's theorem on integral points !