FormalConjectures.Millenium.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.
-/

import FormalConjecturesUtil

The Birch and Swinnerton-Dyer (BSD) Conjecture

References:

The Clay Institute, official problem description by Andrew Wiles: PDF

[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, PDF

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

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

namespace BirchSwinnertonDyeropen scoped Topologyvariable {K : Type*} [Field K] [NumberField K] {E : WeierstrassCurve K}

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



@[category API, AMS 11 14]
theorem IsLFunction.unique {L L' : ℂ → ℂ} (hL : IsLFunction E L) (hL' : IsLFunction E L')
    (x : ℂ) : L =ᶠ[𝓝[≠] x] L' := byK:Type u_1inst✝¹:Field Kinst✝:NumberField KE:WeierstrassCurve KL:ℂ → ℂL':ℂ → ℂhL:IsLFunction E LhL':IsLFunction E L'x:ℂ⊢ L =ᶠ[𝓝[≠] x] L'
  have h2 : meromorphicOrderAt (L - L') 2 = ⊤ := meromorphicOrderAt_eq_top_iff.2 <|
    Filter.Eventually.mono (nhdsWithin_le_nhds <| (Complex.isOpen_re_gt (3 / 2)).mem_nhds
      (byK:Type u_1inst✝¹:Field Kinst✝:NumberField KE:WeierstrassCurve KL:ℂ → ℂL':ℂ → ℂhL:IsLFunction E LhL':IsLFunction E L'x:ℂ⊢ 2 ∈ {z | 3 / 2 < z.re}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' norm_numAll goals completed! 🐙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')) fun s hs => sub_eq_zero.2 ((hL.2 s hs).trans (hL'.2 s hs).symm)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'
  have key : meromorphicOrderAt (L - L') x = ⊤ := not_not.1 fun hx =>
    (hL.1.sub hL'.1).exists_meromorphicOrderAt_ne_top_iff_forall.1 ⟨x, hx⟩ 2 h2K: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'
  exact (meromorphicOrderAt_eq_top_iff.1 key).mono fun s hs => sub_eq_zero.1 hsAll goals completed! 🐙

Hasse--Weil conjecture: the $L$-function of an elliptic curve over a number field extends to the whole plane.

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

The Hasse--Weil conjecture over $\mathbb{Q}$, a consequence of the modularity theorem.

@[category research solved, AMS 11 14]
theorem exists_isLFunction_rat (E : WeierstrassCurve ℚ) [E.IsElliptic] :
    ∃ L, IsLFunction E L := byE:WeierstrassCurve ℚinst✝:E.IsElliptic⊢ ∃ L, IsLFunction E L
  sorryAll goals completed! 🐙

end BirchSwinnertonDyer