Number theory · Algebraic geometry MSC2020 11G05 / 11G40

conjecture

Birch and Swinnerton-Dyer conjecture

OpenGeneral case unresolved

Special cases & conditional resultsRank equality at analytic rank 0 or 1 →Rank-one converse assuming finite Sha →Explore all 6 scoped results →

Still unresolved: Rank equality in general, especially analytic rank ≥ 2, remains open. General finiteness of Sha and the complete leading-coefficient formula are stronger unresolved assertions.

Source report · observed Oct 10, 2026

Source-linked discoveryspecialist backgroundChecked Oct 10, 2026Publication v4

Viewing pinned publication v4. View the current publication →

Question & scope

For an elliptic curve over the rational numbers, does the rank of its rational points equal the order of vanishing of its L-function at s = 1?

Elliptic curves over Q. The canonical question is rank equality. The stronger BSD formula additionally predicts finite Sha and L^(r)(E,1)/(r! Ω_E Reg_E) = #Sha(E/Q) · ∏ c_l / #E(Q)_tors², with the standard full Hasse–Weil L-function, Néron real period, regulator and finite-prime Tamagawa factors. These aspects are tracked separately.

Question paraphrased by OpenMath. Use the cited source and locator for authoritative wording.

Research state

OpenGeneral case unresolved

Rank equality is proved at analytic rank 0 or 1. Further cited results give a conditional converse, selected p-parts and full BSD in specified twist families and finite computations.

Special cases & conditional resultsRank equality at analytic rank 0 or 1 →Rank-one converse assuming finite Sha →Rank-one formula · selected p-parts →Low-rank formula at supersingular p ≥ 5 →Full BSD in a specified infinite twist family →Computer-assisted full formula · 16,714 curves →

Source report · observed Oct 10, 2026 · Clay · Millennium Problems

This curated record attributes the general status and scoped results to their cited sources. Independent mathematical review is pending.

Clay · Millennium Problems

Superseded report

Source label: Unsolved

Source status date unavailable · Observed Oct 1, 2026

The cited source item and version only; this is not an independent OpenMath assessment.

Clay · Millennium Problems

Open

Source label: Unsolved

Source status date unavailable · Observed Oct 10, 2026

The cited source item and version only; this is not an independent OpenMath assessment.

What is established — and under which assumptions

Each result has its own scope and assumptions. Proved implications do not establish their premises; proof barriers and results in related models do not resolve the general question. Counts describe indexed statements, not a percentage solved.

Rank equality & finite Sha

Special case

Rank equality at analytic rank 0 or 1 →

Every E/Q of analytic rank 0 or 1.

E is an elliptic curve over Q.
The full Hasse–Weil L-function has order of vanishing 0 or 1 at s=1.

Limit: No unrestricted analytic-rank ≥ 2 theorem follows.

Exact statement, overlap & source locators

For E/Q with ord_(s=1)L(E,s) equal to 0 or 1, rank E(Q) equals that analytic rank and Sha(E/Q) is finite.

The hypothesis is analytic rank ≤ 1, not merely algebraic rank ≤ 1. This does not alone prove the full leading-coefficient formula.

Skinner · converse to Gross–Zagier–Kolyvagin ↗ · Introduction, journal page 330 (PDF page 2), classical theorem

Wiles · official BSD description ↗ · PDF pages 2 and 4, conjecture/refinement and low-rank theorem

Source: Published

Conditional rank converse

Conditional result

Rank-one converse assuming finite Sha →

Algebraic rank 1 ⇒ analytic rank 1 in this family if Sha is finite.

E/Q is semistable.
E has nonsplit multiplicative reduction at at least one odd prime, or split multiplicative reduction at at least two odd primes.
Algebraic rank E(Q) = 1.
Assume Sha(E/Q) is finite.

Limit: Finite Sha and the reduction hypotheses must be established for an application.

Exact statement, overlap & source locators

For semistable E/Q with nonsplit multiplicative reduction at an odd prime or split multiplicative reduction at two odd primes, algebraic rank 1 and finite Sha imply analytic rank 1.

Runs in the converse direction to the low-analytic-rank theorem. General Sha finiteness is conjectural and is not supplied by assuming algebraic rank 1.

Overlaps with: Rank equality at analytic rank 0 or 1

Skinner · converse to Gross–Zagier–Kolyvagin ↗ · Abstract and Theorem A, journal pages 329–331

Source: Published

Leading coefficient · p-part

Special case

Rank-one formula · selected p-parts →

Good-reduction p ≥ 5 with irreducible E[p], for semistable analytic-rank-one curves.

E/Q is semistable (squarefree conductor N).
ord_(s=1)L(E,s) = 1.
p ≥ 5 is prime and p does not divide N.
The mod-p Galois representation on E[p] is irreducible.

Limit: The missing primes and unrestricted curves require further results.

Exact statement, overlap & source locators

For semistable E/Q of analytic rank 1 and a good-reduction prime p ≥ 5 with E[p] irreducible, the p-adic valuation of L′(E,1)/(Ω_E Reg_E) equals that of #Sha(E/Q) ∏ c_l.

Adds prime-specific leading-coefficient information beyond low-rank equality. Both good ordinary and supersingular reduction are permitted here; the p=3 extension is not included in this selected Claim.

Overlaps with: Rank equality at analytic rank 0 or 1

Jetchev–Skinner–Wan · rank-one BSD p-part ↗ · Theorem 1.2.1, PDF pages 1–2

Source: Published

Leading coefficient · p-part

Special case

Low-rank formula at supersingular p ≥ 5 →

Semistable analytic-rank 0 or 1 at supersingular p ≥ 5.

E/Q is semistable.
ord_(s=1)L(E,s) is 0 or 1.
p ≥ 5 is a prime of good supersingular reduction.

Limit: Other primes and higher analytic ranks are not covered by this selected theorem.

Exact statement, overlap & source locators

For semistable E/Q of analytic rank 0 or 1 and a good supersingular prime p ≥ 5, the p-part of the BSD leading-coefficient formula holds.

Overlaps the supersingular rank-one portion of the Jetchev–Skinner–Wan Claim and additionally includes analytic rank zero. Prime parts are not independent percentages of BSD solved.

Overlaps with: Rank equality at analytic rank 0 or 1 Rank-one formula · selected p-parts

Burungale–Skinner–Tian–Wan · zeta elements ↗ · Theorem 1.5, PDF page 4

Source: Preprint

Leading coefficient · full formula

Special case

Full BSD in a specified infinite twist family →

An infinite, explicitly conditioned family of twists of 46a1.

E/Q is the specific Cremona curve 46a1.
M>1 is squarefree and gcd(M,46)=1; E^M is the twist by Q(√M).
L(E^M,1) is nonzero.
E has ordinary reduction at every prime dividing M.

Limit: Does not give full BSD for every twist, every rank-zero curve, or analytic rank ≥ 2.

Exact statement, overlap & source locators

Let E be Cremona curve 46a1. For squarefree M>1 coprime to 46, if L(E^M,1)≠0 and E has ordinary reduction at every prime dividing M, E^M satisfies full BSD. Infinitely many M meet these conditions.

A full-formula family within the low-analytic-rank case. The 46a1 family is retained after the 2026 Banwait–Huang check; four other base curves in the earlier list have an infinitude caveat.

Overlaps with: Rank equality at analytic rank 0 or 1 Low-rank formula at supersingular p ≥ 5

Burungale–Skinner–Tian–Wan · zeta elements ↗ · Theorem 1.7, PDF page 4, restricted to base curve 46a1

Banwait–Huang · effective BSD twist families ↗ · Section 2.7, v3 PDF page 13

Source: Preprint · Acceptance reported

Leading coefficient · finite corpus

Special case

Computer-assisted full formula · 16,714 curves →

Full formula certified in the paper for 16,714 enumerated curves.

E/Q has conductor <5000 and analytic rank 0 or 1.
E belongs to the successfully certified subset in the cited enumeration, excluding the 11 unresolved curve/prime pairs in Table 9.
Computer-assisted calculations are part of the cited proof; OpenMath has not repeated them.

Limit: The proof does not cover all curves, all conductor ranges or higher analytic ranks.

Exact statement, overlap & source locators

Miller’s computation-assisted proof establishes full BSD for 16,714 of the 16,725 elliptic curves of analytic rank at most one and conductor <5000 in the paper’s enumeration.

Strengthens the formula for a finite subset of the classical low-rank regime. This is computer-assisted proof in the source, not AI theorem discovery or a Lean kernel check.

Overlaps with: Rank equality at analytic rank 0 or 1 Rank-one formula · selected p-parts

Miller · computer-assisted finite BSD cases ↗ · Theorem 1.2 and Table 9, v3 PDF pages 2 and 23

Source: Published

Research activity & artifacts

Recent source updates, computational work and formalization projects provide context. These entries are not counted as additional proved progress. Artifact links carry their own scope and checking status.

source correction

2026 · effective families and an earlier-list caveat

Banwait–Huang give sufficient-condition algorithms for BSD twist subfamilies and list eligible curves of conductor <500,000. Section 2.7 retains 46a1 but identifies a nonempty-prime-support gap for 62a1, 66b1, 105a1 and 141c1 in an earlier infinitude list.

Scope & limitation: The authors do not characterize every BSD-satisfying twist. The flagged four curves are not disproved BSD cases. The code and dataset have not been executed or reproduced by OpenMath.

Banwait–Huang · effective BSD twist families ↗

Barinder S. Banwait · Xiaoyu Huang · Acceptance reported

arXiv metadata reports acceptance for ANTS XVII. Algorithms enumerate sufficient subfamilies, not all curves or twists satisfying BSD.

Paper PDF · v3 ↗Manuscript / exposition · external

Sage algorithms · pinned commit ↗No OpenMath execution recorded

Eligible curve labels · pinned file ↗No OpenMath execution recorded

Revision & attribution

Source revision: arxiv-v3. Observed Oct 10, 2026.

The cited work does not report AI involvement; this is not an assertion that no AI was used.

Source updated Jun 4, 2026.

Paper PDF · v3: arXiv:2601.16044v3. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Sage algorithms · pinned commit: 31fae20c8df3f1f0383f41112b914d4995d5809d. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Eligible curve labels · pinned file: 31fae20c8df3f1f0383f41112b914d4995d5809d. External evidence linked; no OpenMath execution or independent reproduction is asserted.

formalization

AI-assisted exploration · code and Lean targets

This individual AI-augmented research project reports numerical experiments and proof-search scaffolding. Its phase record states that Lean verification has not started; RankEquality.lean contains sorry targets.

Scope & limitation: No new BSD theorem, complete formal proof or OpenMath-verified execution is established by this project citation. Its rank-two regulator identity remains conjectural in the project’s own notes.

Kent · AI-augmented BSD research substrate ↗

Owen P. Kent (repository owner) · Project documentation

Individual project documentation and code; no accepted proof of BSD is asserted by this curation.

Project phase and limitations ↗Source-reported evidence

Computational experiments ↗No OpenMath execution recorded

Lean rank-equality targets ↗Statement only · proof placeholder

The inspected weakBSD and low-rank theorem bodies contain sorry. This is a target skeleton, not a completed formal proof.

Revision & attribution

Source revision: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1. Observed Oct 10, 2026.

README calls the program AI-augmented and contains Claude agent specifications. A precise model version and independently assessed division of labor are not supplied.

Source updated Jun 14, 2026.

Project phase and limitations: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Computational experiments: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Lean rank-equality targets: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1.

computation

2026 · reported rank lower bound 30

The primary record supplies a specific elliptic curve over Q and 30 rational-point witnesses, with a reported rank lower bound of 30.

Scope & limitation: A lower bound on algebraic rank does not establish equality with analytic rank or BSD. OpenMath has not reproduced the independence certificate. Secondary claims of exact rank under BSD+GRH cannot be used as evidence proving BSD.

ICARM · individual high-rank curve record ↗

ICARM leaderboard; submitter ranksunbounded · Project documentation

Public individual curve and rational-point witness record. Verification and AI attribution are not independently established by OpenMath.

Curve and thirty-point witness ↗Source-reported evidence

Revision & attribution

Source revision: observed-2026-10-10. Observed Oct 10, 2026.

Secondary reports associate this search with Claude and Anthropic researchers; the cited primary curve record itself does not establish that attribution, so it is not treated as verified company authorship.

Source updated Aug 20, 2026.

Curve and thirty-point witness: record updated 2026-08-20; observed 2026-10-10. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Literature & sources

Clay problem page and official description ↗

Clay reports the general question unsolved, observed 10 October 2026. This current-state observation is separate from the dated theorem and artifact citations below.

Wiles · official BSD description ↗

Andrew Wiles · Published

Official Clay problem description; separates rank equality from its refined formula.

Official description PDF ↗Manuscript / exposition · external

Revision & attribution

Source revision: official-description. Observed Oct 10, 2026.

The cited work does not report AI involvement; this is not an assertion that no AI was used.

Official description PDF: official-description. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Skinner · converse to Gross–Zagier–Kolyvagin ↗

Christopher Skinner · Published

Annals of Mathematics 191 (2020), 329–354; published online 13 February 2020. Introduction also states the classical low-analytic-rank theorem.

Journal proof PDF ↗Manuscript / exposition · external

Revision & attribution

Source revision: published-online-2020-02-13. Observed Oct 10, 2026.

The cited work does not report AI involvement; this is not an assertion that no AI was used.

Source updated Feb 13, 2020.

Journal proof PDF: Annals 191 (2020), 329–354. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Jetchev–Skinner–Wan · rank-one BSD p-part ↗

Dimitar Jetchev · Christopher Skinner · Xin Wan · Published

Published in Cambridge Journal of Mathematics 5 (2017), 369–434; the cited author preprint supplies Theorem 1.2.1.

Author proof PDF · v1 ↗Manuscript / exposition · external

Revision & attribution

Source revision: arxiv-v1. Observed Oct 10, 2026.

The cited work does not report AI involvement; this is not an assertion that no AI was used.

Source updated Dec 21, 2015.

Author proof PDF · v1: arXiv:1512.06894v1. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Burungale–Skinner–Tian–Wan · zeta elements ↗

Ashay Burungale · Christopher Skinner · Ye Tian · Xin Wan · Preprint

Author preprint at the cited revision; journal acceptance has not been established by this curation.

Proof PDF · v2 ↗Manuscript / exposition · external

Revision & attribution

Source revision: arxiv-v2. Observed Oct 10, 2026.

The cited work does not report AI involvement; this is not an assertion that no AI was used.

Source updated Sep 11, 2024.

Proof PDF · v2: arXiv:2409.01350v2. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Banwait–Huang · effective BSD twist families ↗

Barinder S. Banwait · Xiaoyu Huang · Acceptance reported

arXiv metadata reports acceptance for ANTS XVII. Algorithms enumerate sufficient subfamilies, not all curves or twists satisfying BSD.

Paper PDF · v3 ↗Manuscript / exposition · external

Sage algorithms · pinned commit ↗No OpenMath execution recorded

Eligible curve labels · pinned file ↗No OpenMath execution recorded

Revision & attribution

Source revision: arxiv-v3. Observed Oct 10, 2026.

The cited work does not report AI involvement; this is not an assertion that no AI was used.

Source updated Jun 4, 2026.

Paper PDF · v3: arXiv:2601.16044v3. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Sage algorithms · pinned commit: 31fae20c8df3f1f0383f41112b914d4995d5809d. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Eligible curve labels · pinned file: 31fae20c8df3f1f0383f41112b914d4995d5809d. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Miller · computer-assisted finite BSD cases ↗

Robert L. Miller · Published

LMS Journal of Computation and Mathematics 14 (2011), 327–350. This is the scope of that historical paper, not a current unsolved-case list.

Computer-assisted proof PDF · v3 ↗Manuscript / exposition · external

Revision & attribution

Source revision: arxiv-v3. Observed Oct 10, 2026.

The cited work does not report AI involvement; this is not an assertion that no AI was used.

Source updated Dec 21, 2011.

Computer-assisted proof PDF · v3: arXiv:1010.2431v3. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Kent · AI-augmented BSD research substrate ↗

Owen P. Kent (repository owner) · Project documentation

Individual project documentation and code; no accepted proof of BSD is asserted by this curation.

Project phase and limitations ↗Source-reported evidence

Computational experiments ↗No OpenMath execution recorded

Lean rank-equality targets ↗Statement only · proof placeholder

The inspected weakBSD and low-rank theorem bodies contain sorry. This is a target skeleton, not a completed formal proof.

Revision & attribution

Source revision: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1. Observed Oct 10, 2026.

README calls the program AI-augmented and contains Claude agent specifications. A precise model version and independently assessed division of labor are not supplied.

Source updated Jun 14, 2026.

Project phase and limitations: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Computational experiments: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Lean rank-equality targets: 0e9519aaeb5c8b8c524f95925eecb970d86bc5b1.

ICARM · individual high-rank curve record ↗

ICARM leaderboard; submitter ranksunbounded · Project documentation

Public individual curve and rational-point witness record. Verification and AI attribution are not independently established by OpenMath.

Curve and thirty-point witness ↗Source-reported evidence

Revision & attribution

Source revision: observed-2026-10-10. Observed Oct 10, 2026.

Source updated Aug 20, 2026.

Curve and thirty-point witness: record updated 2026-08-20; observed 2026-10-10. External evidence linked; no OpenMath execution or independent reproduction is asserted.

Provenance & coverage

Coverage of this curation

Rank equality and finite Sha at analytic rank ≤ 1; one conditional converse; selected p-parts; a corroborated infinite twist family; a historical finite-corpus proof. Recent algorithms and AI/Lean exploratory artifacts are separate context.

Formal proofs: No complete Lean proof of the selected BSD Claims has been established here. The inspected individual Lean targets contain sorry; they are explicitly classified as placeholders. No external code has an OpenMath Run or reproduction attached.

AI-assisted work: One self-described AI-augmented individual BSD program is indexed as exploration. High-rank computation is related context, not a BSD proof. No accepted AI-company proof of the general BSD statement was established in this source survey.

Search scope & review

Clay/Wiles; published Skinner and Jetchev–Skinner–Wan papers; author arXiv revisions through June 2026; public code and datasets; Google DeepMind, Axiom, Harmonic, Anthropic-related and individual AI/formalization searches. Cutoff: 10 October 2026. Not exhaustive.

Checked Oct 10, 2026 · independent review pending.

Published after staff preview and source checks. This page covers the cited items; it does not represent a complete list of problems or a literature-wide review.

Selected results, not an exhaustive literature survey or a percentage of the conjecture solved.
Source-attributed theorem statements; independent mathematical and relationship review is pending.
External papers, programs and Lean placeholders have no OpenMath execution or independent reproduction attached.
AI involvement is recorded only where the cited source reports it; absence from this selection does not establish absence of work.

Clay · Millennium Problems ↗

Clay Mathematics Institute · metadata-link · Not established; links and OpenMath paraphrases only

Store metadata and original OpenMath paraphrases; follow the original source for authoritative wording. Rights / source terms

1 cited entry · exact source identity

Version: clay-millennium@observed-2026-10-01
Revision: observed-2026-10-01
Content SHA-256: No upstream byte snapshot retained; linked metadata only
Source update: Unavailable
Observed: 2026-10-01
Check cadence: 30 days

https://www.claymath.org/millennium/birch-and-swinnerton-dyer-conjecture/ ↗birch-and-swinnerton-dyer-conjecture:entry:0:v1

Clay · Millennium Problems ↗

Clay Mathematics Institute · metadata-link · Not established; links and OpenMath paraphrases only

Store metadata and original OpenMath paraphrases; follow the original source for authoritative wording. Rights / source terms

1 cited entry · exact source identity

Version: clay-millennium@observed-2026-10-10
Revision: observed-2026-10-10
Content SHA-256: No upstream byte snapshot retained; linked metadata only
Source update: Unavailable
Observed: 2026-10-10
Check cadence: 30 days

https://www.claymath.org/millennium/birch-and-swinnerton-dyer-conjecture/ ↗birch-and-swinnerton-dyer-conjecture:entry:0:v2

Wiles · official BSD description ↗

Andrew Wiles · metadata-link · Links and original OpenMath paraphrases only; upstream license governs external files.