Growth of $f(n)=\sum_{p<n}1/(n-p)$: liminf, limsup, and an $o(\log\log n)$ bound (Erdős #950)
Statement
For a positive integer $n$, let $$f(n)=\sum_{p<n}\frac{1}{n-p},$$ where the sum runs over all primes $p<n$. Erdős asks: is it true that $$\liminf_{n\to\infty} f(n)=1\quad\text{and}\quad \limsup_{n\to\infty} f(n)=\infty?$$ And is it true that $f(n)=o(\log\log n)$ for all $n$?
Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, else full written proof) of the asserted values $\liminf f(n)=1$ and $\limsup f(n)=\infty$, and of $f(n)=o(\log\log n)$; a proof of any one of the three claims in isolation counts if clearly delimited. ADVANCES: improve the best-known lower bound on $\liminf f(n)$ beyond the status stated in background (which only gives $>0$ conditional on short-interval prime counts) — e.g. an unconditional positive lower bound, or $\liminf\geq 1$ under a clearly stated hypothesis; prove $f(n)=o(\log\log n)$ or any nontrivial upper bound on the growth of $f(n)$ (for instance making the conditional $f(n)\ll\log\log\log n$ unconditional or strengthening it); or establish $\sum_{p<x}f(p)^2\sim\pi(x)$ for the prime-restricted analogue. Purely numerical exploration supports an ADVANCES claim only when paired with the exact program and the certified range. Deliver the proof or formalisation, plus any accompanying reproducible computation and the ranges covered.
Background
Posed by Erdős [Er77c, p.63]; listed as open on erdosproblems.com/950 (fetched 2026-07-21, status 'open'). The average behaviour is understood: de Bruijn, Erdős, and Turán showed $\sum_{n<x}f(n)\sim\sum_{n<x}f(n)^2\sim x$; they gave no proofs, and a proof of the harder second-moment asymptotic was later supplied by Ofir Gorodetsky (2025, on MathOverflow). Toward the liminf, the mere existence of some $c>0$ for which $[n,n+n^c]$ always contains $\gg n^c/\log n$ primes would already force $\liminf f(n)>0$. Erdős proposed a weaker, 'perhaps not quite inaccessible' conjecture: for every $\epsilon>0$ and all large $x$ there is $y<x$ with $\pi(x)<\pi(y)+\epsilon\,\pi(x-y)$ (compare the distinct SciNet problem at erdosproblems.com/855 on $\pi(x+y)\leq\pi(x)+\pi(y)$). He further noted that if $\pi(x)<\pi(y)+O((x-y)/\log x)$ for all $y<x-(\log x)^C$ then $f(n)\ll\log\log\log n$. The analogue $f(p)$ along primes is harder still — Erdős could not even prove $\sum_{p<x}f(p)^2\sim\pi(x)$. A Lean formalisation exists in the DeepMind formal-conjectures repository; no cash prize is attached. Attacker's tool: direct high-range computation of $f(n)$ from sieved prime tables to probe the liminf$\to 1$, limsup$\to\infty$, and $f(n)/\log\log n$ behaviour, combined with prime-counting / short-interval estimates and the de Bruijn–Erdős–Turán moment method.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #950 (T. F. Bloom) | website |
| REF-02 | Gorodetsky — proof of the de Bruijn–Erdős–Turán second-moment asymptotic (MathOverflow) | website |
| REF-03 | Lean formalisation (DeepMind formal-conjectures) — Erdős #950 | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.