Must an infinite real set with $\lvert kx-y\rvert\geq 1$ for all pairs and all $k\geq 1$ be sparse? (Erdős #143)
Statement
Let $A\subset(1,\infty)$ be a countably infinite set of reals with the separation property $$\lvert kx-y\rvert\geq 1\qquad\text{for all distinct }x,y\in A\text{ and all integers }k\geq 1.$$ (When $A$ consists of integers this condition forces $A$ to be primitive: no element divides another.) Must such a set be 'sparse'? Concretely, must the reciprocal-log sum converge, $$\sum_{x\in A}\frac{1}{x\log x}<\infty,$$ or at least must the partial reciprocal sum be small, $$\sum_{\substack{x\in A\\ x<n}}\frac{1}{x}=o(\log n)?$$
Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, given the existing Lean formalisation) either that every such $A$ satisfies $\sum_{x\in A}1/(x\log x)<\infty$, or a construction of a set $A\subset(1,\infty)$ with $\lvert kx-y\rvert\geq1$ for all distinct $x,y$ and all $k\geq1$ whose reciprocal-log sum diverges, settling the \$500 question negatively. ADVANCES: a quantitative sparsity bound strictly stronger than the known $\sum_{x<n}1/x=o(\log n)$ of [KLL25] (the bound stated in background) — for instance a Behrend-type $\ll\log x/\sqrt{\log\log x}$ estimate valid for real $A$ — with full proof; or a verified explicit construction of such $A$ whose reciprocal sum provably approaches the current upper bound. Deliver the proof / Lean file or the certified construction.
Background
A recurring question of Erdős [Er61, Er73, Er77c, Er80 p.101, Er92c, Er97c]; in [Er97c] he offered \$500 for the questions in the main statement. Listed as open on erdosproblems.com/143 (fetched 2026-07-21, status 'open'). Context from the integer (primitive-set) case: Erdős [Er35] proved $\sum_{n\in A}1/(n\log n)$ converges for primitive $A$; Behrend [Be35] proved $\sum_{n<x}1/n\ll\log x/\sqrt{\log\log x}$, sharpened to $o(\cdot)$ by Erdős, Sárközy and Szemerédi [ESS67]; and Haight (unpublished, cited in [Er73, Er77c]) showed the counting density tends to $0$ when the elements are $\mathbb{Q}$-independent. Key recent progress: Koukoulopoulos, Lamzouri and Lichtman [KLL25] proved the weaker of the two displayed alternatives, $\sum_{x<n}1/x=o(\log n)$, for all such real sets — so the $o(\log n)$ question is now settled and the remaining, prize-carrying, open question is the stronger convergence $\sum_{x\in A}1/(x\log x)<\infty$. The problem is formalised in Lean; see also erdosproblems.com/858. Attacker's tool: analytic number theory extending the Behrend / [KLL25] machinery toward the convergence bound, and, on the constructive side, searching for real sets $A$ obeying $\lvert kx-y\rvert\geq1$ with anomalously large reciprocal-log sums to probe sharpness or force divergence.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #143 (T. F. Bloom) | website |
| REF-02 | Lean formalisation of Erdős #143 (DeepMind formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.