Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

Anne Baanen; Alex J. Best; Nirvana Coppola; Sander R. Dahmen

doi:10.1145/3573105.3575682

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

Anne Baanen^*, Alex J. Best, Nirvana Coppola, Sander R. Dahmen

^*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form y2=x3+d, where d is a (given) nonzero integer number and all solutions in integers x and y have to be determined. One non-elementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of d<0. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover, we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond.

Original language	English
Title of host publication	CPP 2023
Subtitle of host publication	Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
Editors	Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic
Publisher	Association for Computing Machinery, Inc
Pages	47-62
Number of pages	16
ISBN (Electronic)	9798400700262
DOIs	https://doi.org/10.1145/3573105.3575682
Publication status	Published - Jan 2023
Event	12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023 - Boston, United States Duration: 16 Jan 2023 → 17 Jan 2023

Conference

Conference	12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023
Country/Territory	United States
City	Boston
Period	16/01/23 → 17/01/23

Bibliographical note

Funding Information:
Anne Baanen was funded by NWO Vidi grant No. 016.Vidi. 189.037, Lean Forward. Alex J. Best, Nirvana Coppola, and Sander R. Dahmen were funded by NWO Vidi grant No. 639.032.613, New Diophantine Directions.

Publisher Copyright:
© 2023 Owner/Author.

Keywords

algebraic number the- ory
Diophantine equations
formalized mathematics
Lean
Mathlib
tactics

Access to Document

10.1145/3573105.3575682

Persistent URL (handle)

Copy link address

Cite this

Baanen, A., Best, A. J., Coppola, N., & Dahmen, S. R. (2023). Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. In R. Krebbers, D. Traytel, B. Pientka, & S. Zdancewic (Eds.), CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 47-62). Association for Computing Machinery, Inc. https://doi.org/10.1145/3573105.3575682

Baanen, Anne ; Best, Alex J. ; Coppola, Nirvana et al. / Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. editor / Robbert Krebbers ; Dmitriy Traytel ; Brigitte Pientka ; Steve Zdancewic. Association for Computing Machinery, Inc, 2023. pp. 47-62

@inproceedings{cbfcb20766a1426b8c007a1bdd3826e8,

title = "Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves",

abstract = "Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form y2=x3+d, where d is a (given) nonzero integer number and all solutions in integers x and y have to be determined. One non-elementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of d<0. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover, we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond.",

keywords = "algebraic number the- ory, Diophantine equations, formalized mathematics, Lean, Mathlib, tactics",

author = "Anne Baanen and Best, {Alex J.} and Nirvana Coppola and Dahmen, {Sander R.}",

note = "Funding Information: Anne Baanen was funded by NWO Vidi grant No. 016.Vidi. 189.037, Lean Forward. Alex J. Best, Nirvana Coppola, and Sander R. Dahmen were funded by NWO Vidi grant No. 639.032.613, New Diophantine Directions. Publisher Copyright: {\textcopyright} 2023 Owner/Author.; 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023 ; Conference date: 16-01-2023 Through 17-01-2023",

year = "2023",

month = jan,

doi = "10.1145/3573105.3575682",

language = "English",

pages = "47--62",

editor = "Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka and Steve Zdancewic",

booktitle = "CPP 2023",

publisher = "Association for Computing Machinery, Inc",

}

Baanen, A, Best, AJ, Coppola, N & Dahmen, SR 2023, Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. in R Krebbers, D Traytel, B Pientka & S Zdancewic (eds), CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, Inc, pp. 47-62, 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023, Boston, United States, 16/01/23. https://doi.org/10.1145/3573105.3575682

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. / Baanen, Anne; Best, Alex J.; Coppola, Nirvana et al.
CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. ed. / Robbert Krebbers; Dmitriy Traytel; Brigitte Pientka; Steve Zdancewic. Association for Computing Machinery, Inc, 2023. p. 47-62.

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

AU - Baanen, Anne

AU - Best, Alex J.

AU - Coppola, Nirvana

AU - Dahmen, Sander R.

N1 - Funding Information: Anne Baanen was funded by NWO Vidi grant No. 016.Vidi. 189.037, Lean Forward. Alex J. Best, Nirvana Coppola, and Sander R. Dahmen were funded by NWO Vidi grant No. 639.032.613, New Diophantine Directions. Publisher Copyright: © 2023 Owner/Author.

PY - 2023/1

Y1 - 2023/1

N2 - Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form y2=x3+d, where d is a (given) nonzero integer number and all solutions in integers x and y have to be determined. One non-elementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of d<0. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover, we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond.

AB - Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form y2=x3+d, where d is a (given) nonzero integer number and all solutions in integers x and y have to be determined. One non-elementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of d<0. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover, we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond.

KW - algebraic number the- ory

KW - Diophantine equations

KW - formalized mathematics

KW - Lean

KW - Mathlib

KW - tactics

UR - http://www.scopus.com/inward/record.url?scp=85147005431&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85147005431&partnerID=8YFLogxK

U2 - 10.1145/3573105.3575682

DO - 10.1145/3573105.3575682

M3 - Conference contribution

AN - SCOPUS:85147005431

SP - 47

EP - 62

BT - CPP 2023

A2 - Krebbers, Robbert

A2 - Traytel, Dmitriy

A2 - Pientka, Brigitte

A2 - Zdancewic, Steve

PB - Association for Computing Machinery, Inc

T2 - 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023

Y2 - 16 January 2023 through 17 January 2023

ER -

Baanen A, Best AJ, Coppola N, Dahmen SR. Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. In Krebbers R, Traytel D, Pientka B, Zdancewic S, editors, CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, Inc. 2023. p. 47-62 Epub 2023 Jan 11. doi: 10.1145/3573105.3575682

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

Abstract

Conference

Bibliographical note

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this