OpenAI claim summary for Math-2945
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
Avoiding affine dyadic sequences: The primary statement says: For every eta>0 there is a compact subset of [0,1] of measure greater than 1-eta containing no affine copy of {2^(-n):n>=1}, with either sign of nonzero dilation. The target retains these quantified objects and hypotheses, so its positive assertion is covered.
With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Avoiding every dyadic affine sequence in a large-measure set
OpenAI's claim
Avoiding affine dyadic sequences: The dyadic paper claims compact subsets of $[0,1]$ with measure arbitrarily near one that omit at least one point of every translated, nontrivially dilated dyadic sequence. Positive and negative dilation parameters are both included.Mathematical statement of the claimed result
Mathematical claim 1.
For every $0<\eta<1$ there is compact $E_\eta\subset[0,1]$ with Lebesgue measure $m(E_\eta)>1-\eta$ such that \[\forall x\in\mathbb R\ \forall s\ne0\ \exists n\ge1:\quad x+s2^{-n}\notin E_\eta.\] Thus no nonconstant affine copy of the entire dyadic sequence is contained in $E_\eta$.Outline of the argument
Avoiding affine dyadic sequences: A sparse periodic hitting set is built from random tables on an ordered finite tree. Routes preserved by suitable dyadic shifts provide many fresh terminal tests, while the edge-wise scale count is beaten by their failure probability. A small open repair handles exceptional centers; rescaling and reflection extend the hitting property to all nonzero signed scales.Formal verification
Family 084 describes Lean coverage for avoidance for the dyadic ratio; it does not assert avoidance for an arbitrary geometric ratio.Avoiding affine dyadic sequences: The manuscript links DyadicAvoidance.lean.
The documented selection does not cover the entire manuscript assertion relevant here.
This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.
Status caveat
OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.Sources
- OpenAI, The dyadic case of the Erdős similarity conjecture, 2026-09-25; citation key
OAI:The-dyadic-case-of-the-Erdos-similarity-conjecture-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 084: Lean scope.
- Comparator DyadicAvoidance.json.
- Comparator DyadicAvoidance.lean.
- OpenAI catalogue entry.