Formalized Class Group Computations and Integral Points on Mordell Elliptic Curve...
summary
Formalization proves integer solutions for several Mordell equations, notably y^2 = x^3 - 13 with x = 17, y = ±70, by formalizing ideal norms, quadratic rings and explicit class group computations in Lean 3 (~6k LOC). The work computes the class group and shows its order is coprime to 3 so cube-factorization arguments hold, implements a new computation tactic times_table_tac for finite-basis rings, and connects to external CAS via Sage; the tactics and integrations run and complete the needed algebraic and analytic bounds.
AI-written summary · about
chapters (9)
- 0:00Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
- 0:44This project
- 5:07Classical number theory tools
- 6:56Using these sort of techniques
- 10:24THE ARGUMENT
- 13:03When do cubes only factor into cubes?
- 15:07BOUNDING CLASS GROUPS
- 17:09CALCULATIONAL TACTICS
- 18:58CONNECTION TO COMPUTER ALGEBRA SYSTEMS