1. FormalConjectures
  2. Millennium
  3. BSD
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import FormalConjecturesUtil

The Birch and Swinnerton-Dyer (BSD) Conjecture

References:

    The Clay Institute, official problem description by Andrew Wiles: claymath.org

    [BSD1965] B. J. Birch and H. P. F. Swinnerton-Dyer. "Notes on elliptic curves. II." Journal fur die reine und angewandte Mathematik 218 (1965), 79-108, doi

    [Tate1966] John Tate. "On the conjectures of Birch and Swinnerton-Dyer and a geometric analog." Seminaire Bourbaki, Vol. 9, Exp. No. 306 (1966), 415-440, numdam

    [Gross2011] Benedict H. Gross. "Lectures on the conjecture of Birch and Swinnerton-Dyer." Arithmetic of L-functions, IAS/Park City Math. Ser. 18, AMS (2011), 169-209, math.harvard.edu

    [Ang2025] David Kurniadi Angdinata. "L-functions of Dirichlet twists of elliptic curves: computations and congruences." PhD thesis, University College London (2025), discovery.ucl.ac.uk

    [Ada] Tom Adamczewski. "Autoformalized conjectures", Birch and Swinnerton-Dyer

@[expose] public sectionnamespace BSDopen scoped Topologysection NumberFieldvariable {K : Type*} [Field K] [NumberField K] {E : WeierstrassCurve K}

L is an $L$-function of E: it is meromorphic on $\mathbb{C}$ and agrees with the $L$-series of E on $\operatorname{Re} s > 3/2$, where that series converges.

The $L$-function is expected to be holomorphic, and IsHolomorphicLFunction is that stronger notion, but meromorphy is all that is needed to state the Birch and Swinnerton-Dyer conjecture. [Gross2011] states the conjecture under this hypothesis, and we take that form as authoritative.

def IsLFunction (E : WeierstrassCurve K) (L : ℂ → ℂ) : Prop := Meromorphic L ∧ ∀ s : ℂ, 3 / 2 < s.re → L s = E.LSeries s

L is a holomorphic $L$-function of E: it is entire and agrees with the $L$-series of E on $\operatorname{Re} s > 3/2$. This is the continuation Hasse and Weil conjectured.

def IsHolomorphicLFunction (E : WeierstrassCurve K) (L : ℂ → ℂ) : Prop := Differentiable ℂ L ∧ ∀ s : ℂ, 3 / 2 < s.re → L s = E.LSeries s@[category API, AMS 11 14] theorem IsHolomorphicLFunction.isLFunction {L : ℂ → ℂ} (hL : IsHolomorphicLFunction E L) : IsLFunction E L := ⟨fun z ↦ (hL.1.analyticAt z).meromorphicAt, hL.2⟩

An $L$-function is determined by the $L$-series it continues: two of them agree on a punctured neighbourhood of every point. They need not agree at a pole.

K:Type u_1inst✝¹:Field Kinst✝:NumberField KE:WeierstrassCurve KL:ℂ → ℂL':ℂ → ℂhL:IsLFunction E LhL':IsLFunction E L'x:ℂh2:meromorphicOrderAt (L - L') 2 = ⊤⊢ L =ᶠ[𝓝[≠] x] L' K:Type u_1inst✝¹:Field Kinst✝:NumberField KE:WeierstrassCurve KL:ℂ → ℂL':ℂ → ℂhL:IsLFunction E LhL':IsLFunction E L'x:ℂh2:meromorphicOrderAt (L - L') 2 = ⊤key:meromorphicOrderAt (L - L') x = ⊤⊢ L =ᶠ[𝓝[≠] x] L' All goals completed! 🐙

Weak Hasse--Weil conjecture: the $L$-series of an elliptic curve over a number field has a meromorphic continuation to the whole plane. This is weaker than what Hasse and Weil conjectured, and is the form the Birch and Swinnerton-Dyer conjecture is stated under.

@[category research open, AMS 11 14] theorem exists_isLFunction (E : WeierstrassCurve K) [E.IsElliptic] : ∃ L, IsLFunction E L := K:Type u_1inst✝²:Field Kinst✝¹:NumberField KE:WeierstrassCurve Kinst✝:E.IsElliptic⊢ ∃ L, IsLFunction E L All goals completed! 🐙

Hasse--Weil conjecture: the $L$-series of an elliptic curve over a number field has a holomorphic continuation to the whole plane.

@[category research open, AMS 11 14] theorem exists_isHolomorphicLFunction (E : WeierstrassCurve K) [E.IsElliptic] : ∃ L, IsHolomorphicLFunction E L := K:Type u_1inst✝²:Field Kinst✝¹:NumberField KE:WeierstrassCurve Kinst✝:E.IsElliptic⊢ ∃ L, IsHolomorphicLFunction E L All goals completed! 🐙end NumberFieldsection Ratvariable (E : WeierstrassCurve ℚ) [E.IsElliptic]

The Hasse--Weil conjecture over $\mathbb{Q}$, a consequence of the modularity theorem: the $L$-series of an elliptic curve over $\mathbb{Q}$ has a holomorphic continuation.

@[category research solved, AMS 11 14] theorem exists_isHolomorphicLFunction_rat : ∃ L, IsHolomorphicLFunction E L := E:WeierstrassCurve ℚinst✝:E.IsElliptic⊢ ∃ L, IsHolomorphicLFunction E L All goals completed! 🐙end Rat

The weak Birch and Swinnerton-Dyer conjecture for a number field $K$: for every elliptic curve $E$ over $K$, a meromorphic continuation of its $L$-series has order $\operatorname{rank}_{\mathbb{Z}} E(K)$ at $s = 1$.

The rank is AddCommGroup.freeRank, which requires $E(K)$ to be finitely generated. That is the Mordell--Weil theorem, which Mathlib does not have and which this repository states as a sorry in EllipticCurveRank.mordell_weil, so it appears here as a hypothesis.

def Weak (K : Type*) [Field K] [NumberField K] [DecidableEq K] : Prop := ∀ (E : WeierstrassCurve K) [E.IsElliptic] [AddGroup.FG E.toAffine.Point] (L : ℂ → ℂ), IsLFunction E L → meromorphicOrderAt L 1 = AddCommGroup.freeRank E.toAffine.Point

Weak Birch and Swinnerton-Dyer conjecture ([Tate1966], Conjecture (A)).

@[category research open, AMS 11 14] theorem weak_birch_swinnerton_dyer_conjecture (K : Type*) [Field K] [NumberField K] [DecidableEq K] : Weak K := K:Type u_1inst✝²:Field Kinst✝¹:NumberField Kinst✝:DecidableEq K⊢ Weak K All goals completed! 🐙

The weak Birch and Swinnerton-Dyer conjecture over $\mathbb{Q}$, a Clay Millennium Prize Problem.

@[category research open, AMS 11 14] theorem weak_birch_swinnerton_dyer_conjecture_rat : Weak ℚ := ⊢ Weak ℚ All goals completed! 🐙end BSD