Generalized Riemann Hypothesis for Selberg class

### What is the conjecture

The **Selberg class** $\mathcal{S}$ is the axiomatic class of Dirichlet series $F(s) = \sum_{n=1}^{\infty} \frac{a_n}{n^s}$ satisfying four axioms:

1. **Analyticity and growth:** $F(s)$ is analytic except possibly at $s=1$, and satisfies suitable growth conditions in vertical strips.
2. **Functional equation:** There exist parameters $Q > 0$, a positive integer $d$, and complex numbers $\mu_j$ (with $\text{Re}(\mu_j) \geq 0$) such that
$$\chi(s) := Q^s \prod_{j=1}^{d} \Gamma(\mu_j s + \lambda_j) F(s)$$
satisfies $\chi(s) = \overline{\chi(1-\overline{s})}$ for some choice of $\lambda_j$.

3. **Euler product:** $F(s)$ has an Euler product, expressing it as $\prod_{p \text{ prime}} \sum_{k=0}^{\infty} \frac{b_{p,k}}{p^{ks}}$.
4. **Ramanujan hypothesis:** For each prime $p$, the coefficients $b_{p,k}$ satisfy $|b_{p,k}| \leq 1$.

The **Generalized Riemann Hypothesis for the Selberg class** asserts that:

$$\text{For all } F \in \mathcal{S}, \text{ every non-trivial zero of } F \text{ lies on the critical line } \text{Re}(s) = \tfrac{1}{2}.$$

This conjecture unifies classical Riemann Hypothesis (for the Riemann zeta function), the generalized Riemann hypothesis for Dirichlet $L$-functions, and the conjectures for many other arithmetically important $L$-functions (Dedekind zeta functions, Artin $L$-functions, etc.) under a single axiomatic framework.

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

**Sources:**
- https://en.wikipedia.org/wiki/Generalized_Riemann_hypothesis#Generalized_Riemann_hypothesis_for_Selberg_class, https://arxiv.org/abs/1511.04603, https://arxiv.org/abs/2410.22711, https://en.wikipedia.org/wiki/Selberg_class

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Basic complex analysis and analytic functions (Mathlib has foundational definitions)
- Dirichlet series (partial support in Mathlib)
- Functional equations of L-functions (minimal support)

Missing pieces (exactly 2; unclear/absent from search results):
- Formal axiomatic definition of the Selberg class with all four axioms (analyticity, functional equation, Euler product, Ramanujan hypothesis)
- Theory of zero-location for L-functions and critical line properties

Rating justification: The Selberg class is a specialized axiomatic framework not present in Mathlib. While basic analytic function concepts exist, the sophisticated machinery needed to formalize the definition of Selberg class (with functional equations and growth conditions) and the notion of zeros lying on a critical line would require significant new theory infrastructure beyond current Mathlib capabilities.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-11
* ams-30

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] 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](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

No repository file, test, or entry point is named. Start by reviewing the cited Selberg-class sources and existing formalized conjectures in the repository, then determine what definitions and infrastructure are missing. Done means the conjecture is added as a checked Lean formalization, with appropriate supporting theory and tests if the project provides them.

Written by the indexing model from the issue text.