Exponent pair conjecture

### What is the conjecture

An **exponent pair** is a pair of real numbers $(k, \ell)$ with $0 \le k \le 1/2 \le \ell \le 1$ such that for all sufficiently smooth phase functions $F$ and all $T \ge N \ge 1$, every subinterval $I \subseteq [N, 2N]$ satisfies the exponential sum bound:
$$\sum_{n \in I} e(TF(n/N)) \ll_{\epsilon} (T/N)^{k+\epsilon} N^{\ell+\epsilon}$$
for all $\epsilon > 0$.

The **exponent pair conjecture** states that every point $(k, \ell)$ in the triangular region $\{(k, \ell) : 0 \le k \le 1/2 \le \ell \le 1, k + \ell \le 1\}$ is an exponent pair. Equivalently, the conjecture asserts that the pair $(0, 1/2)$ is an exponent pair.

This conjecture has major consequences: it implies the Lindelöf hypothesis and provides square-root cancellation bounds for exponential sums arising in analytic number theory.

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

**Sources:**
- - [Wikipedia: Van der Corput's method](https://en.wikipedia.org/wiki/Van_der_Corput%27s_method)
- [Exponent Pair Database (GitHub)](https://github.com/teorth/expdb)
- [New exponent pairs, zero density estimates, and zero additive energy estimates: a systematic approach](https://arxiv.org/html/2501.16779)
- [Toward optimal exponent pairs](https://arxiv.org/html/2306.05599)
- [Van der Corput's Method and the Theory of Exponent Pairs (Oxford Academic)](https://academic.oup.com/qjmath/article-abstract/6/1/147/1572543)

### Prerequisites needed

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

Building blocks (1-3; from search results):
- `Real.exp` and complex exponential functions (available in Mathlib)
- Finset summation and asymptotic notation $O()$, $o()$ (available in Mathlib.Data.Asymptotic)
- Function smoothness/differentiability conditions (available in Mathlib.Analysis.Calculus)

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of "phase function" with the specific smoothness/boundedness constraints required for the van der Corput method
- Theory of exponential sums and bounds on them, including the technical definition of how exponent pairs apply to different classes of sums

Rating justification (1-2 sentences): The basic mathematical infrastructure (exponentials, sums, asymptotic notation) exists in Mathlib, but the conjecture requires developing the specialized theory of exponent pairs and exponential sums from scratch. This is significant new theory that, while not foundational, would require multiple interconnected definitions and lemmas specific to analytic number theory.

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

* ams-11

### 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)

Start by reading the conjecture definition and the cited exponent-pair sources, then inspect the repository's existing formalized conjectures for the expected statement structure. The issue names no target file, test, or formal entry point; completion would require defining the missing phase-function and exponential-sum theory and formalizing the conjecture.

Written by the indexing model from the issue text.