#120: OpenAI claims the geometric case of the Erdős similarity conjecture — for every ratio q a compact set of measure 1 − η with no affine copy of {qⁿ}; four hostile seats read the 13-page proof and found no gap, and the dyadic case (Green's Problem 94) is a Lean theorem that our kernel replay accepts

The problem (erdosproblems.com/120; Erdős 1974, Mathematica Balkanica 4, Problem 4.33.7*; $100). Let A ⊆ ℝ be infinite. Must there be a set E ⊂ ℝ of positive measure containing no set of the shape aA + b, a ≠ 0? Call A measure universal if the answer is no — if every measurable set of positive measure contains an affine copy of A. Steinhaus's theorem makes every finite set universal (translate the set by s·a for each of the finitely many a; for small s the intersection still has positive measure), so the conjecture says exactly that no infinite set is. It is true when A is unbounded or dense in an interval, so the content is a sequence a₁ > a₂ > … → 0. Falconer (1984) and Eigen (1985) settled every sequence with a_n+1/a_n → 1; Kolountzakis (1997), Humke–Laczkovich (1998) and Chlebík (2015) gave finite-gap criteria that need the normalized minimum gap of large finite subsets to decay subexponentially in their size; Bourgain (1987) handled sums of three infinite sets. Geometric sequences fail every one of those criteria (the gap is at most q^m−2/(1 − q) for m points), which is why the page can say the problem "is open when A = {1, 1/2, 1/4, …}, which is Problem 94 on Green's open problems list" and Chlebík could write in 2015 that the status of every geometric or faster sequence was unknown.

The claim. OpenAI's 6 October 2026 release (github.com/openai/math, 372 claims) carries two unsigned preprints on this problem, both in Bloom's 8 October list of 23 Erdős problems the release touches ("a special case of the Erdős similarity problem"). The dyadic case of the Erdős similarity conjecture (25 September, 16 pp): for every η ∈ (0,1) there is a compact E_η ⊆ [0,1] with m(E_η) > 1 − η such that for every x ∈ ℝ and s ≠ 0 some x + s2⁻ⁿ, n ≥ 1, lies outside E_η. The geometric case of the Erdős similarity conjecture (5 October, 13 pp): the same for {qⁿ : n ≥ 1} and every fixed q ∈ (0,1), the set depending on q. Both signs of the dilation are included; the paper is explicit that it says nothing about arbitrary infinite sets. The release's Lean formalizes the dyadic statement only (OAI.Problem310.dyadic_affine_avoidance, 75 modules, 8,455 lines, Mathlib-only imports); the general-ratio theorem is paper only.

Why it stayed open, and what gets past it. The natural attack is Kolountzakis's: a random union of grid cells at resolution ≈ q⁻ⁿ for each index n, so that for a fixed centre x and scale t the points x + tqⁿ are tested independently. The obstruction is that the densities p_n must be summable — the open set has to be small — and then ∏(1 − p_n) is bounded below, so each (x, t) is missed with a fixed probability while there are uncountably many of them; splitting a single budget p across r indices gives a miss probability like e^−pr against about q^−2r distinct configurations as t sweeps [1,2], which loses. The two incomplete UBC summer reports the paper cites (Solymosi 2011, Tom 2015) stopped there. The new idea is to spend the measure budget once and the resolution freely: every point of the line is routed down a complete M-ary tree of height d by independent fair-bit tables indexed by nested dyadic grids (first child whose bit is 1, else the default last child), and only the leaf carries a Bernoulli-p table deciding membership — so the random set B has density exactly p however deep the tree (Lemma 4.1). Each edge owns a window of consecutive indices n, laid out in preorder with gaps; a centre is stable if translations from a window never move it across a boundary of any earlier grid (Lemma 3.2: all but density 4Kcq^g+1 of centres), while at the window's own resolution the centre and its r translated points have distinct keys (Lemma 3.3, because the cell width is below (1 − q)q^b). At a stable centre whose route first takes a default at vertex U — which happens unless an event of probability (1 − 2^1−M)^d — the translated points of the windows on U's non-default edges inherit the centre's earlier decisions, reach U, and read fresh bits (Lemma 4.2); conditional on the centre's exposed entries, the (M − 1)r local tests fail together with probability exactly (1 − p/2)^(M−1)r at any fixed scale (Lemma 4.3). The step that makes the scale count affordable is the window-length rule r_h ≥ g + σ_h−1 (Lemma 3.1): a test at the first default consults no grid finer than 2r indices past its window's start, so as t sweeps [1,2] the vector of local tests changes at most D_M,q(r) = 4 + 2(M − 1)r(1 + 2cq^−2r) times (Lemma 5.1), a count that does not depend on M — and choosing M with p(M − 1)/2 > 2 log(1/q) makes the exponential win. Missed centres form a closed periodic set of density ≤ 3p, covered by an open set that repairs them because tqⁿ → 0; the resulting open periodic H of density ≤ 6p hits x + tG_q for every centre and every t ∈ [1,2] (Proposition 2.1), and a summable union of dyadic dilations and reflections of such sets, p_k = η4^−|k|/64, removes measure exactly 7η/16 from [0,1] while meeting every nontrivial affine copy (§2).

What we did. Four hostile seats (Opus, tool-equipped, disjoint scopes, each briefed with the paper's architecture and told to quote the sentence it objects to): grids (§3), routing (§4), scales (§5 and §2), and a whole-paper seat aimed at the question above — why fifty years, and where would it break. All four: HOLDS AS READ, every lemma in both papers verified line by line, no FATAL, no GAP. The objections are cosmetic and listed in the reports: the nesting identity and the monotonicity of window endpoints are asserted rather than proved (the dyadic paper writes them out); Lemma 4.3 carries a "stable centre" hypothesis it never uses; the step 1 − u ≤ e^−u in Lemma 5.1 is implicit; the measurability of x ↦ ℙ(x ∈ R) is unstated (trivial on a finite probability space); the Chlebík repair citation is looser than in the dyadic version; the notation 𝒜 clashes with A_i,n. The "prove too much" tests all came back the right way: the argument uses the infinitude of the pattern in exactly two places — the index sets must grow as p → 0 (from (5.5), (M − 1)r_* > 2 log(4/p)/p) and the repair step needs tqⁿ → 0 — so for a finite pattern it proves only the true "most centres" statement, consistent with Steinhaus; the geometric ratio enters at Lemmas 3.2 and 3.3 and in the count (5.3), which depends only on the index difference, so a super-geometric sequence breaks (5.3) and the method does not reach the full conjecture; for q → 1 every constant stays finite for each fixed q (the paper never claims uniformity). Three seats ran the paper's own construction in exact rational arithmetic as an instrument that can fail: the routing seat measured the conditional failure probability in 48 cells (two centres including a grid-boundary point, U at heights 1 and 2, generic and boundary scales, p ∈ {0.3, 0.5}) against (1 − p/2)^(M−1)r — max |z| 2.14 over 98 z-scores, success counts binomial — with 0 violations of Lemma 4.2 in 26.9 million translated-point routings, while an unstable centre broke Lemma 4.2, a 64× coarser grid broke the formula (z = +135) and a mutated membership rule broke the density (z = +362); the whole seat repeated it on six configurations at q ∈ {1/2, 3/5, 1/3} to depth 3 with the same pattern; the grids seat laid out the windows of 36 trees and found Lemma 3.1 sharp (equality at every height ≥ 2), 0 key collisions in Lemma 3.3, 0 violations of (3.3) in 250,000 comparisons at stable centres. Our own script (checks/checks120.py, written from the definitions): the measure sum (2.3) is 7/16 exactly in rationals; (3.1), monotonicity and the separation inequality hold for q from 0.03 to 0.999 with margin ≥ 4; Lemma 3.1 on the 36 trees; (4.3) by Monte Carlo; the finite r_* of (5.5) exists at five (q, p) pairs (r_* = 93 at q = 1/2, p = 1/2; 7,030 at q = 1/3, p = 0.05, where the slack over 2 log(1/q) is 0.003); and an exact-rational Monte Carlo of Lemma 4.3 on our own implementation of the construction (four instances, q ∈ {1/2, 1/3, 7/10}, 1,000 samples each under a 4 GB memory cap) lands within 1σ of (1 − p/2)^(M−1)r every time — 0.328 vs 0.316, 0.420 vs 0.422, 0.518 vs 0.512, 0.323 vs 0.316 — with 0 violations of Lemma 4.2 and densities 0.49–0.51 at p = 1/2, plus Lemma 5.1's |T| ≤ D on every vertex of two trees (the root's breakpoint count, ~2·10²¹ at r = 33, is counted arithmetically, not enumerated). One thing the brief got wrong and the seats caught: a toy with gap g = 1 admits no stable centre at all — the paper's choice of g rules exactly that out, and the simulations used the paper's g.

The Lean, and what it certifies. The comparator (ComparatorChallenges/DyadicAvoidance.lean) states, with a sorry: for every η ∈ (0,1) there is E ⊆ [0,1], compact, of volume > 1 − η, such that for all x, s with s ≠ 0 some x + s·(1/2)ⁿ, n ≥ 1, is outside E. That is the page's special case verbatim up to one line: a compact set is measurable, and an affine copy of {1, 1/2, 1/4, …} contains an affine copy of {1/2, 1/4, …}, so avoiding the latter avoids the former (Formal Conjectures' green_94 quantifies n from 0; same remark). Our replay, lake-free: the 75 modules of the import cone compiled in topological order with Lean v4.34.1 against Mathlib d13f23b7 (818 s, 0 errors, Mathlib's cache fetched fresh, nothing of OpenAI's build reused); then with --trust=0 the kernel reports that dyadic_affine_avoidance and periodic_hitting_set depend only on propext, Classical.choice, Quot.sound; the pp.all statement printed from the proof module is byte-identical (2,426 characters; replay/statement_match.txt, row statement_match_v2) to the one printed from the comparator compiled on its own, and so is the definition of dyadicPoint; the comparator's sorry shows up as sorryAx (so the probe can see a sorry); a hand-retyped copy of the statement is inhabited by the theorem, and the same statement with 1 − η/2 in place of 1 − η is rejected with a type mismatch. A source scan of the 75 files finds no sorry, axiom, native_decide, unsafe or implemented_by; the only external import root is Mathlib. leanchecker --fresh over the whole import closure — Mathlib's cache re-checked by the external checker, not just our 75 modules — exited 0 after 3,849 s (64 min; it prints nothing on a pass); its controls: a non-existent module exits 1 with "Could not find any oleans", the non-fresh check of a single module exits 0. (One instrument note, kept in the bundle: the driver's first statement-comparison script raised a false alarm — it keyed on a character the output does not print and did not strip universe suffixes from axiom names; the kernel's own logs were correct throughout and the corrected comparison is a literal block equality.) A provenance point all four seats raised independently: the Lean proves the dyadic paper's construction, which at q = 1/2 is not the geometric paper's specialization — its grids are 2^b+2 against the geometric N_b = 2^b+3, its branching condition is p(M − 1)/2 ≥ 10 against > 2 log 2, and its final deduction uses only shrinking dilations together with 2^−mD ⊆ D, which is special to q = 1/2, where the geometric §2 uses every k ∈ ℤ. Each version is internally correct and their scale-count constants agree where they overlap; but the kernel certifies the dyadic theorem, not a line of the geometric proof. The general-ratio bookkeeping rests on the seats' hand checks above. Independently of us, Harald Schilly's math-distance-set-similarity (Zenodo, October 2026) reports rebuilding OpenAI's whole 2,459-file Lean tree at commit adc7f12 under leanchecker --fresh and uses the dyadic theorem as an explicit hypothesis; the module is byte-identical between that commit and today's main.

The world, 14 October. The problem page (last edited 23 January 2026) still says the dyadic case is open; the proof-claims tab is empty; of the three comments, two (14 March 2026) concern a different statement — Formal Conjectures had once omitted measurability, a DeepMind prover found that the ℤ-span of a Hamel basis has positive outer measure and avoids every affine copy of {1, 1/2, 1/4, …}, and a reader notes de Reyna (1983) proved that outer-measure variant for every |A| ≥ 3 — and one (November 2025) points to Gao–Mooroogen–Yip on a Kolountzakis–Papageorgiou analogue. Green's list (30 January 2026 version) still asks Problem 94 ("Let A ⊂ ℝ be a set of positive measure. Does A contain an affine copy of {1, 1/2, 1/4, …}?") with no update. The teorth database says open (statement formalized, last updated 31 August 2025 — refreshed today). Formal Conjectures has moved: PR #6898, merged 11 October, marks green_94 research solved, answer(False), citing OpenAI's Main.lean#L103; erdos_120 — the general conjecture — stays open, which is the right pair. Bloom's 8 October post lists #120 among the 23 with his standing caveat that he has not read the proofs or checked that the Lean compiles. The sources seat fetched every reference of both papers at the cited version — all fifteen exist, all seven arXiv version stamps match the archive's history, and twenty-two characterisations of cited results match their sources (Chlebík's Theorem 15 in its σ-form; Kolountzakis's Theorem 3 and his §3.4 on D + D; the two-fold-sumset paper's Theorem 2, whose introduction says in so many words that the single sequence {2⁻ⁿ} "remains open"; the Rajchman paper's Theorem 1.5 and Propositions 3.2 and 4.1). Two things the papers should have said: the Jung–Lai–Mooroogen survey (arXiv:2412.11062, Res. Math. Sci. 2025) calls deciding whether (2⁻ⁿ) is measure universal "the major bottleneck of the problem" and its Question 7.2 — "Let b > 1 be a real number. Is there a set of positive measure containing no sequence (x + yb⁻ⁿ) for any x, y with y ≠ 0?" — is exactly Theorem 1.1, uncited; and the locator "Problem 4.33.7*" for Erdős's 1974 Mathematica Balkanica item appears in no source independent of OpenAI (the literature cites the item as pp. 203–204 or 197–202 with no sub-number). Novelty: every pre-release source, the latest dated 1 August and 3 September 2026, calls the case open; nothing earlier proves it. What has happened since is downstream of OpenAI: Jiang–Xi (arXiv:2610.11449, 8 October) run the same finite-tree construction for every null sequence with liminf a_n+1/a_n > 0 and say plainly that it stops where that liminf is 0 — consistent with the seats' reading of where the geometric ratio enters; Schilly's replay above; and seventeen MathOverflow threads about the release, none of which mentions this problem. Humke's three-page Notices piece of August 2026 could not be fetched (403, unarchived). No human verification or refutation of either paper exists anywhere the seat looked.

Labels. The dyadic case, Green's Problem 94, answered NO: (d) computer-assisted — a kernel-checked proof exists, written by the claimant, source-audited here, and our own replay printed the three standard axioms on a statement matched to the challenge, with a third-party replay on record. The geometric case for every ratio (Theorem 1.1 of the 5 October paper): (c) plausible/unverified by a human — four tool-equipped machine seats with disjoint scopes read it line by line, each briefed to refute, and found no gap; the probabilistic core was reproduced by simulation with controls that fail. The §2 reduction from the periodic hitting set to the theorem, the 7η/16 budget, and the one-line bridge to the problem page's statement: (a) elementary, checked here. Scoreboard: #120 stays OPEN — the conjecture is about every infinite set, and nothing here touches that; the family {qⁿ}, which the page names as the open special case, is now claimed for every q and formally proved for q = 1/2. Not ours.