Skip to content
Cairn Commons
X Sign in
Level A · Machine-checkable Hard Number theory P-hasse-weil

The Hasse–Weil conjecture for elliptic curves

The L-series of an elliptic curve over a number field has a meromorphic continuation to ℂ.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Start working on it Submit a claim Follow
Cite 
@misc{cairn-hasse-weil,
  title        = {The Hasse–Weil conjecture for elliptic curves},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/hasse-weil}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-28}
}

Also: CITATION.cff · Atom feed of results

Claims
0
Verified
0
Disputed
0
Refuted
0
On the literature board
0

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

The question

exists_hasMeromorphicContinuation. The -series of an elliptic curve over a number field has a meromorphic continuation to . This is the Hasse--Weil conjecture in the form stated in [Wikipedia], a weak form of [Gross2011], Conjecture 2.7, and the hypothesis under which the Birch and Swinnerton-Dyer conjecture is stated ([Gross2011], Conjecture 2.10).

exists_hasAnalyticContinuation. The Hasse--Weil conjecture ([Tate1966], p. 416; [Gross2011], Conjecture 2.7): the -series of an elliptic curve over a number field has an analytic continuation to .

The -series of an elliptic curve over a number field converges absolutely on ([Tate1966], p. 416; [Gross2011], Lecture 2, §1). The Hasse--Weil conjecture predicts that it has an analytic continuation to the whole complex plane and satisfies a functional equation ([Tate1966], p. 416; [Gross2011], Conjecture 2.7, stated there for the completed -function). Only the continuation is stated here. Over it follows from the modularity theorem.

[Wikipedia] states the conjecture for the Hasse--Weil zeta function and asks only for a meromorphic continuation, which is equivalent to a meromorphic continuation of . This is also the hypothesis under which the Birch and Swinnerton-Dyer conjecture is stated ([Gross2011], Conjecture 2.10), so the weaker continuation is recorded here as well.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.HasseWeil (2 statements).

theorem exists_hasMeromorphicContinuation (E : WeierstrassCurve K) [E.IsElliptic] :
    ∃ L, HasMeromorphicContinuation E L
theorem exists_hasAnalyticContinuation (E : WeierstrassCurve K) [E.IsElliptic] :
    ∃ L, HasAnalyticContinuation E L

What counts as progress

  • A Lean proof of one of the statements above, pinned as the claim's formal statement.
  • Partial results: special cases, weaker bounds, reductions — as verified claims.
  • Computations and numerical evidence with published code (reproducible).
  • Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
  • A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

  • Wikipedia
  • [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

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.