Skip to content

Extended Riemann Hypothesis (ERH) for Dedekind Zeta Functions #2376

@franzhusch

Description

@franzhusch

What is the conjecture

The Extended Riemann Hypothesis (ERH) concerns zeros of Dedekind zeta functions of algebraic number fields. Let $K$ be an algebraic number field and let $\zeta_K(s)$ denote its Dedekind zeta function. The Extended Riemann Hypothesis asserts that every non-trivial zero of $\zeta_K(s)$ that lies in the critical strip ${s \in \mathbb{C} : 0 < \text{Re}(s) < 1}$ has real part equal to $\frac{1}{2}$. Equivalently, all such zeros lie on the critical line $\text{Re}(s) = \frac{1}{2}$. The ERH is a natural generalization of the classical Riemann Hypothesis from the Riemann zeta function to the broader class of Dedekind zeta functions.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

Sources:

Prerequisites needed

Formalizability Rating: 3/5 (0 is best) (as of 2026-02-21)

Building blocks (1-3; from search results):

  • Algebraic number field structures (available in Mathlib)
  • Basic complex analysis and analytic continuation (available in Mathlib)
  • Special function definitions (some support in Mathlib)

Missing pieces (exactly 2; unclear/absent from search results):

  • Dedekind zeta function definition and its analytic properties for general number fields
  • Characterization of the critical strip and zeros of analytic functions in the required form

Rating justification (1-2 sentences): Formalizing the ERH statement requires developing the full theory of Dedekind zeta functions (definition, meromorphic continuation, functional equation) for arbitrary number fields, which is substantial new infrastructure not present in Mathlib. However, once these definitions exist, the conjecture statement itself can be formulated relatively directly.

AMS categories

  • ams-11
  • ams-12
  • ams-30

Choose either option

  • I plan on adding this conjecture to the repository
  • This issue is up for grabs: I would like to see this conjecture added by somebody else

This issue was generated by an AI agent and reviewed by me.

See more information here: link

Feedback on mistakes/hallucinations: link

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions