Elliott–Halberstam conjecture

[franzhusch]

What is the conjecture

The Elliott–Halberstam conjecture concerns the uniform distribution of primes in arithmetic progressions. For a modulus $q$, let $\theta(x;q,a) = \sum_{\substack{p \leq x \ p \equiv a \pmod{q}}} \log p$ denote the weighted sum of primes in the arithmetic progression $a \pmod{q}$ up to $x$, where the weight is $\log p$. The error term is defined as $E(x;q) := \max_{(a,q)=1} \left| \theta(x;q,a) - \frac{x}{\varphi(q)} \right|$, measuring the deviation from the expected uniform distribution (where $\varphi$ is Euler's totient function). The conjecture asserts: for every $0 < \vartheta < 1$ and every $A > 0$, $$\sum_{q \leq x^{\vartheta}} \max_{y \leq x} |E(y;q)| \ll \frac{x}{(\log x)^A}$$ where the implied constant depends only on $\vartheta$ and $A$. This states that the total error in prime distribution across all moduli up to $x^{\vartheta}$ is bounded by $x/(\log x)^A$.

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

Sources:

• https://en.wikipedia.org/wiki/Elliott%E2%80%93Halberstam_conjecture, https://arxiv.org/abs/2511.14810, https://arxiv.org/abs/1410.7073, https://terrytao.wordpress.com/tag/elliott-halberstam-conjecture/, https://msp.org/ant/2015/9-4/ant-v9-n4-p09-s.pdf

Prerequisites needed

Formalizability Rating: 2/5 (0 is best) (as of 2026-04-03)

Building blocks (from Mathlib):

• Nat.Prime: predicate for primes
• ZMod: modular arithmetic and residue classes
• Nat.totient: Euler's totient function
• Asymptotic analysis (Big-O notation) in Asymptotics

Missing pieces:

• Chebyshev theta function: a weighted sum of logarithms of primes in arithmetic progressions, requiring careful formalization of the restricted prime sum
• Formalization of the maximum error term $E(x;q)$ over all coprime residue classes, and the nested max in the main bound

Rating justification: The core mathematical objects (primes, modular arithmetic, asymptotic notation) are well-established in Mathlib. However, formalizing the specific Chebyshev theta function for arithmetic progressions and the error term requires non-trivial definitions, making this moderately straightforward but not immediate.

AMS categories

• ams-11

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.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link