楕円曲線の階数は、その L 関数の零点の位数と一致するか？（BSD 予想）

有理数体上の任意の楕円曲線について、その有理点群の階数が、Hasse-Weil L 関数の s = 1 における零点の位数と等しいかを決定せよ。

Decide whether, for every elliptic curve over the rationals, the rank of its group of rational points equals the order of vanishing of its Hasse-Weil L-function at s = 1.

A Clay Millennium Prize Problem. The rank 0 and rank 1 cases are theorems (Gross-Zagier, Kolyvagin); nothing is known for rank at least 2, and the methods that settle the low-rank cases do not extend.

解決したかどうかは、問いではなくアプローチごとに決まります。Atlas は判定しません。外部の判定者が何をしたかを記録します。

• Lean 4 formalization (formal-conjectures)

  形式証明

  到達状況

  未着手

  判定者

  the Lean 4 typechecker, against the pinned toolchain · 型検査

  定式化

  Existence and properties of the L-function of an elliptic curve, stated in Lean 4 as the first step toward the full conjecture.問いより弱いLean v4.33.1 + mathlib@0df444a3 (formal-conjectures@fc2696b2)検証対象を見る

  保たれているもの

  • The analytic object the conjecture is about

  弱まっているもの

  • Does not yet state the rank equality itself

  加えられた仮定・条件

  • The Lean file formalizes existence of the L-function rather than the full rank statement, so the formal target is weaker than the question

  Statement only, and only part of the way to the conjecture.

• Heegner points and Euler systems

  査読付きの証明

  到達状況

  進行中

  判定者

  the number theory community, through journal peer review · 査読

  定式化

  Use Heegner point constructions and Euler systems to relate the rank to the behaviour of the L-function.問いより弱い

  保たれているもの

  • Settles the conjecture completely for analytic rank 0 and 1

  弱まっているもの

  • The construction produces at most one independent point, so it cannot reach rank 2 or higher

  加えられた仮定・条件

  • Modularity and the theory of complex multiplication

  閉じた道

  • Heegner point methods produce a single point, so they are structurally incapable of proving rank at least 2 cases; the open part of the conjecture needs a different source of rational points.無条件
    • paperV. A. Kolyvagin, Euler systems, The Grothendieck Festschrift II (1990) 435-483Rank 0 and 1 cases of the Birch and Swinnerton-Dyer conjecture

  証拠

  • paperdoi:10.1007/BF01388809B. Gross, D. Zagier, Heegner points and derivatives of L-series, Invent. Math. 84 (1986) 225-320
  • paperV. A. Kolyvagin, Euler systems, The Grothendieck Festschrift II (1990) 435-483Rank 0 and 1 cases of the Birch and Swinnerton-Dyer conjecture

• Numerical verification for curves of small conductor

  計算による判定

  到達状況

  進行中

  判定者

  execution against published curve databases · 実行

  定式化

  Compute ranks and L-function vanishing orders for large families of curves and compare.問いより弱い

  保たれているもの

  • Confirms the equality for every curve tested

  弱まっているもの

  • Finitely many curves; rank computations assume finiteness of the Tate-Shafarevich group in places

  加えられた仮定・条件

  • Trust in the algorithms and in unproved assumptions used by rank algorithms

  閉じた道

  • Verification for finitely many curves cannot settle a statement about all of them, and the algorithms themselves lean on conjectures.無条件
    • standardhttps://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdfA. Wiles, The Birch and Swinnerton-Dyer conjecture, Clay Mathematics Institute official problem description

• repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Millennium/BSD.lean:85
• standardhttps://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdfA. Wiles, The Birch and Swinnerton-Dyer conjecture, Clay Mathematics Institute official problem description

URI

https://atlasalt.com/q/4298f3ac-f054-4cf9-ad15-587a354a4f4a

登録

2026-09-17

最終レビュー

2026-09-19

次回レビュー期限

2027-09-19

版

65317227d10e

ライセンス

CC-BY-4.0

立場

record_only（Atlas は判定しない）