Is the longest arithmetic progression of primes in $\{1,\ldots,N\}$ of length $o(\log N)$? (Erdős #200)
Statement
Let $L(N)$ denote the length of the longest arithmetic progression consisting entirely of primes, all of whose terms lie in $\{1,\ldots,N\}$. Does the longest arithmetic progression of primes in $\{1,\ldots,N\}$ have length $o(\log N)$? That is, is $L(N)/\log N\to 0$ as $N\to\infty$?
Acceptance. FULLY RESOLVES: a proof that $L(N)=o(\log N)$, or a proof that $\limsup L(N)/\log N>0$ (e.g. by producing prime APs of length $\ge c\log N$ in $[N]$ for some explicit $c>0$ and infinitely many $N$). Machine-checkable (Lean/Coq) proof preferred — the formal-conjectures statement can host it — else a complete written proof with all steps; a computation alone cannot close this. ADVANCES: any proven improvement of the constant in the upper bound $L(N)\le(1+o(1))\log N$ stated in the background; a proven lower bound for $L(N)$ growing faster than what Green–Tao-type arguments currently give (state and beat the comparison explicitly); or a reproducible computational study — exact values of $L(N)$ up to a record height with exhaustive-search certificate and code, or an extension of OEIS A005115 by at least one new confirmed term — presented with the empirical $L(N)/\log N$ trajectory as evidence, clearly flagged as non-proof. Deliver the proof file, or the search code + certificates + new terms/tables.
Background
A problem of Erdős and Graham [ErGr79] [ErGr80]; listed as open on erdosproblems.com/200 (fetched 2026-07-13, status 'open', tagged 'primes | arithmetic progressions'). The upper frontier is classical: a length-$k$ prime AP inside $[N]$ must have common difference divisible by every prime below $k$, and via the prime number theorem this forces $L(N)\le(1+o(1))\log N$ — the question is whether this trivial bound is asymptotically lossy. On the lower side, the Green–Tao theorem guarantees $L(N)\to\infty$, but with bounds enormously far from $\log N$; unconditionally nothing close to the truth is known. Empirically, the longest explicitly known prime APs have around 27 terms (found by large distributed searches in the 2010s–2020s), and OEIS A005115 tabulates the minimal final term of an arithmetic progression of $n$ primes — exactly the data that traces the empirical growth of $L(N)$ against $\log N$. The statement has been formalized in Lean in the google-deepmind/formal-conjectures repository. The attacker's tools: on the computational side, exhaustive sieve-based computation of $L(N)$ (or extensions of A005115) to new record ranges to compare the empirical curve with $c\log N$; on the proof side, refined Hardy–Littlewood-type heuristics made rigorous on average, or improvements to the primorial-difference argument.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #200 (T. F. Bloom) | website |
| REF-02 | OEIS A005115 — minimal final term of an arithmetic progression of n primes | website |
| REF-03 | Lean formalization of Erdős #200 (google-deepmind/formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.