Erdős Problem #120
Erdős similarity problem

Read our full write-up →

Erdős asked whether every infinite set A ⊂ ℝ is avoided by some set of positive measure — no x + sA inside it, s ≠ 0. Finite sets are never avoided (Steinhaus); slowly decaying sequences are (Falconer, Eigen); the live page says the question is open for A = {1, 1/2, 1/4, …}, Problem 94 on Ben Green's list. OpenAI's 6 October release carries two anonymous preprints: a 16-page proof for the dyadic sequence (25 September, formalized in Lean) and a 13-page proof for every geometric sequence {qⁿ}, 0 < q < 1 (5 October, paper only). We read both. The construction routes every point of the line through a finite tree of random fair-bit tables and spends its measure budget exactly once at the leaf, so the number of independent chances to hit a translated point grows without the density growing; the scale count stays local to one block of the tree. Four tool-equipped seats with disjoint scopes, each briefed to refute, verified every lemma line by line and found only cosmetic items; exact-arithmetic simulations of the paper's own construction match its exact probability formula and the negative controls fail. OpenAI's own Lean proof of the dyadic case — Green's Problem 94 exactly — was kernel-replayed on our machine today: all 75 modules compiled against Mathlib's pinned commit, the main theorem depends only on the three standard axioms, its statement is byte-identical to the challenge, the wrong-shape control fails, and leanchecker --fresh over the whole import closure exited 0. The general conjecture — every infinite set — stays open; what is settled, pending human review, is the family of geometric progressions, the special case the problem page names as open.