{"id":"palomar/PALOMAR-2026-10-16-000002","url":"https://github.com/pmaronow/ec567-palomar/tree/b1f2ded85275d67b78fada55212fefff54d7c35e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000002-v1.json","repo":"https://github.com/pmaronow/ec567-palomar","tags":["math.NT","msc:11G05","msc:11N32","elliptic-curves","number-theory","formal-verification","lean"],"score":0,"title":"Elliptic curves of exact ranks five, six, and seven: conditional formalization","trust":"high","domain":"math.NT","source":"palomar","authors":["P. M. Aronow","Patrick Lopatto"],"reviews":0,"subject":"math.NT","summary":"Lean proves that the finite-complexity affine-linear prime asymptotic implies infinitely many geometric isomorphism classes of rational elliptic curves of each exact Mordell–Weil rank five, six, and seven. The generic analytic theorem is an explicit hypothesis. The specialization checks, two-isogeny descent, exact rank calculations, and passage to infinitely many j-invariants are formalized; the prime asymptotic is not proved in Lean here.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Infinitely Many Elliptic Curves of Exact Ranks Five, Six, and Seven","identifier":"sha256:5d3f85d7f6a07c8e8382f2629a49449689746655b0c4d2edb319b0197523e75a","relationship":"adapts"}]}