Open Research Index

Elliptic curves of exact ranks five, six, and seven: conditional formalization

P. M. Aronow, Patrick Lopatto

Palomar Registrypalomar/PALOMAR-2026-10-16-000002Oct 16, 2026math.NTscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-16-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'