Browse › Real and complex analysis › 084 The geometric case of the Erdős similarity conjecture
The dyadic case of the Erdős similarity conjecture
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We construct a compact subset of the unit interval, of measure arbitrarily close to one, that contains no affine copy of the dyadic sequence $\{2^{-n}:n\ge1\}$. The conclusion holds for every translation and every nonzero real dilation, of either sign, proving the dyadic case of the Erdős similarity conjecture.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Kan Jiang and Lifeng Xi, The Erdős similarity problem for null sequences with adjacent ratios bounded below (arXiv:2610.11449, 8 October 2026). Builds compact sets of measure above $1-\eta$ in $[0,1]$ that avoid affine copies of positive null sequences with $\liminf a_{n+1}/a_n>0$ (without monotonicity, and simultaneously for prescribed countable families), adapting the finite-tree construction of the dyadic and geometric manuscripts, which it cites as unpublished manuscripts [17, 18]. [family-level]
- Harald Schilly, Erdős similarity for distance sets: finite patterns, a pinned obstruction, and an open window (preprint and Lean repository, October 2026). This follow-up, prepared with substantial Claude assistance, derives pinned-distance obstructions from the avoidance results and reports replaying the dyadic Lean proof, while retaining general-ratio avoidance as an explicit hypothesis. [family-level]
Formalization
- OpenAI math release, Lean scope note for family 084 (release Lean documentation). Describes a Lean formalization of Theorem 1.1 (compact $E\subset[0,1]$, $m(E)>1-\eta$, avoiding $x+s2^{-n}$ for all $x$ and both signs of $s\neq0$). [family-level]
- OpenAI math release, DyadicAvoidance/Main.lean (openai/math, commit adc7f12). Contains the Lean theorem
Problem310.dyadic_affine_avoidance, derived from a periodic hitting-set lemma. [family-level] - google-deepmind/formal-conjectures, GreensOpenProblems/94.lean (formal-conjectures, accessed 2026-10-21). States Green's Open Problem 94 (the dyadic case), marks it
research solvedciting this paper, and links the OpenAI Lean proof; the statement in this file ends insorry. - mo271, feat: mark problems solved in the OpenAI math release and link formal proofs (formal-conjectures PR #6898, merged 11 October 2026). Lists "Green 94 (dyadic Erdős similarity)" among the newly solved problems; a commenter asked whether Erdős Problem 120 should also be updated, and the merged change does not include it.
Related prior literature mentioned by others
- Yeonwook Jung, Chun-Kit Lai, Yuveshen Mooroogen, Fifty years of the Erdős similarity conjecture (arXiv:2412.11062v2, 2025-01-01). This survey states the conjecture "remains open for exponentially decaying sequences" and reviews variants of measure universality; Jiang–Xi and Schilly cite it, and it is not in this paper's bibliography.
Possibly relevant literature (found by the agent, not checked)
- Alex Burgin, Samuel Goldberg, Tamás Keleti, Connor MacMahon, Xianzhi Wang, Large sets avoiding infinite arithmetic / geometric progressions (arXiv:2210.09284, October 2022). Builds a compact set with a density point at 0 that contains no non-constant infinite geometric progression, a variable-ratio variant of the avoidance of affine copies of $\{2^{-n}\}$ in Theorem 1.1; not in this paper's bibliography.
Digests and expositions
- Patrick White with Claude, Erdős Problem a Day, Erdős #120: OpenAI claims the geometric case (2026-10-14). Explains the routing and scale-counting construction and reports AI-led proof audits and a dyadic Lean replay, explicitly distinguishing these from human verification of the general-ratio theorem. [AI-generated per source] [family-level]
Elsewhere
- Emergent Mind: family 084
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:The-dyadic-case-of-the-Erdos-similarity-conjecture-September-25-2026,
author = {{OpenAI}},
title = {{The dyadic case of the Erd\H{o}s similarity conjecture}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/The-dyadic-case-of-the-Erdos-similarity-conjecture-September-25-2026/paper.pdf}{OAI:The-dyadic-case-of-the-Erdos-similarity-conjecture-September-25-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/084.md. The Lean statements have not been checked by people against the paper's claims.
Family 084: The geometric case of the Erdős similarity conjecture
For every fixed $q\in(0,1)$, constructs compact subsets of $[0,1]$ with measure arbitrarily close to one containing no translated and nontrivially dilated copy of $\{q^n:n\ge1\}$, with dilations of either sign. This resolves the geometric-progression case of the Erdős similarity conjecture for every ratio.
Other papers in this family:
- The geometric case of the Erdős similarity conjecture · October 5, 2026