The Erdős similarity conjecture
The Erdős similarity conjecture asks whether, for every infinite set A of real numbers, there is a measurable set of positive Lebesgue measure that contains no affine copy x + sA with s ≠ 0. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September and 5 October 2026, treat the cases of the dyadic and geometric sequences. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original results
- Dyadic case. For every η in (0, 1) there is a compact subset of [0, 1] of measure greater than 1 − η that contains no affine copy of {2−n : n ≥ 1}, for every translation and every nonzero real dilation of either sign.
- Geometric case. For every fixed q in (0, 1) and every η in (0, 1) there is a compact set of measure greater than 1 − η in [0, 1] containing no nontrivial affine copy of {qn : n ≥ 1}. The set may depend on q; the manuscript makes no simultaneous assertion for different ratios.
- Sources (openai/math repository, commit
1581d4c): - Formalization, as described by the repository. The scope note lean/docs/084.md states that the Lean formalization proves the dyadic case: for every 0 < η < 1, a compact set in [0, 1] of measure greater than 1 − η containing no affine copy of {2−n}, for both signs of the dilation. The geometric case for general q is outside that statement.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Harald Schilly, math-distance-set-similarity (Zenodo preprint 10.5281/zenodo.23219651) | Use | Studies whether the distance set of a compact set of large Hausdorff dimension must contain an affine copy of the dyadic sequence, combining the dyadic case with the collection's Falconer distance theorem; a Lean 4 formalization and a paper. | The repository shows a Lean build workflow; the paper is a Zenodo preprint. |
| 2026-10-08 | K. Jiang and L. Xi, arXiv:2610.11449 | Extension | For every positive null sequence with lim inf an+1/an > 0, and every η > 0, a compact subset of [0, 1] of measure greater than 1 − η containing no nontrivial affine copy of the sequence; no monotonicity is assumed. The abstract describes the proof as an adaptation of a finite-tree construction for geometric sequences; the body credits that construction to the collection's dyadic and geometric manuscripts. | arXiv preprint, version 1. |
| 2026-10-10 | Vjekoslav Kovač, Hexagon record 2610.00176v1 | Extension | A non-universality criterion beyond geometric decay, covering decreasing positive null sequences with log(1/an) = o(n log log n) and log(an/an+1) ≥ e−nα eventually, for some 0 < α < 1. The record states that the manuscript was generated by ChatGPT-6 Astra, which was asked to build on the geometric-case manuscript, and that the proof modifies its finite-tree construction. | Hexagon labels: primarily AI-generated text; human understanding: some parts. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.