---

Claim. Let $D=\{2^{-n}:n\ge1\}$. For every $\eta\in(0,1)$ there is a compact set $E\subseteq[0,1]$ of Lebesgue measure greater than $1-\eta$ such that for every $x\in\mathbb{R}$ and every $s\in\mathbb{R}\setminus\{0\}$ some $n\ge1$ has $x+s2^{-n}\notin E$; that is, $E$ contains no set $aD+b$ with $a\ne0$, for either sign of $a$. This is Theorem 1.1 of The dyadic case of the Erdős similarity conjecture, a manuscript of the OpenAI mathematics release dated 25 September 2026, whose author line is "OpenAI" and whose release README says the manuscripts were produced by an internal OpenAI model and that the collection includes results at different stages of verification; the claimant is the organization. The statement is compiled on the result page theorem_1_1 and the digest on the card openai_2026_dyadic_case_erdos_similarity_conjecture. The proof reduces the theorem to a periodic hitting lemma: for every $p\in(0,1)$ an open $1$-periodic set of density at most $6p$ meets $x+tD$ for every real $x$ and every $t\in[1,2]$. The lemma is proved by routing the points of the line through a finite ordered tree whose edges carry windows of dyadic indices, with random selector tables and Bernoulli terminal tests, and by an open-cover repair of the exceptional centers; a summable union of dyadic dilations and reflections of the hitting sets is then removed from $[0,1]$. Since the question of Problem 120 asks for such an $E$ for every infinite $A$, the theorem is the case $A=D$ and no more; it answers the site's named open special case, the dyadic sequence, and is the $q=1/2$ instance of the release's later geometric-progression claim, which does not cite it.

Covers. Our question, answered yes for the single set $A=\{2^{-n}:n\ge1\}=\{1/2,1/4,1/8,\ldots\}$. For every $\eta\in(0,1)$ there is a compact set $E$ inside $[0,1]$ with Lebesgue measure greater than $1-\eta$, so positive. $E$ contains no set $aA+b$ for any real $b$ and any nonzero $a$ of either sign. The theorem does not cover other infinite sets, including other geometric sequences $\{q^n\}$, or the general question. The only extra sets that follow are sets containing a nonzero affine copy of this one, by a one-line argument that is not in the Lean.

Acceptance. Formalized, as a partial claim. This corpus's verification built OAI.Problem310.dyadic_affine_avoidance at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and checked its axioms, which are exactly propext, Classical.choice and Quot.sound, with no sorry; the comparator challenge lean/ComparatorChallenges/DyadicAvoidance.lean pins the declaration with its definition dyadicPoint, and its fingerprint was found identical to the challenge. A statement audit unfolded the declaration to Mathlib and found that it states the Claim above clause by clause: dyadicPoint n is $2^{-n}$ and the bound $n\ge1$ gives exactly $D$; the volume is Lebesgue measure, and the bound above ENNReal.ofReal (1 - η) is a genuine real bound, since $1-\eta>0$, which forces positive measure; the quantifiers over every real $x$ and every nonzero $s$ exclude each copy $x+sD$, for both signs of $s$; and the conclusion is not met trivially, since the empty set has measure zero and $[0,1]$ contains $\tfrac12D$. The declaration settles Problem 120 for the single set $A=D$, equivalently for the site's named case $\{1,1/2,1/4,\ldots\}=2D$, whose affine copies are those of $D$. The extension to sets containing an affine copy of $D$ is not in the Lean, and the general question is untouched, so the scope stays partial. Not reviewed: the manuscript has no refereed publication and no arXiv version, no reviewer independent of the claimant has endorsed it, and the release's README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification. The site's commentary names the dyadic sequence as an open case of the conjecture (Problem 94 on Green's list), and its proof-claims tab carried no claim for this problem; the survey of Jung, Lai and Mooroogen records the conjecture as open for exponentially decaying sequences such as $2^{-n}$. Read depth: the theorem statement, clause by clause, on the result page; no proof step of the manuscript was checked.

Formalization. The release's Lean page for its family 084 names this manuscript as its accompanying paper and describes the formalized statement as the dyadic case above, both signs of the dilation included. The comparator statement file lean/ComparatorChallenges/DyadicAvoidance.lean states OAI.Problem310.dyadic_affine_avoidance (the label 310 is the release's own numbering, not Erdős Problem 310) with the definition OAI.Problem310.dyadicPoint n = (2:ℝ)⁻¹ ^ n, and its companion configuration points to the solution module OAI/MeasureTheory/DyadicAvoidance/Main.lean and permits the axioms propext, Classical.choice and Quot.sound. The pinned statement quantifies over every $\eta\in(0,1)$ and asks for a compact $E\subseteq[0,1]$ of volume above ENNReal.ofReal (1 - η) such that for all real $x$ and nonzero $s$ some $n\ge1$ has $x+s\cdot2^{-n}\notin E$, which is the theorem as stated. The supporting declarations are OAI.Problem310.periodic_hitting_set and OAI.Problem310Support.avoidance_of_periodic_hitting. The build and the statement audit of the pinned declaration are recorded in the Acceptance paragraph above.

Depends on. Nothing beyond the cited manuscript.