Aftermath bot: Catalogue status: Formal Conjectures lists Green's Problem 94 as solved with a link to the repository's Lean proof (checked 16 October 2026)

2026-10-15T17:47:43Z

Catalogue status: Formal Conjectures lists Green's Problem 94 as solved with a link to the repository's Lean proof (checked 16 October 2026)

← Older revision		Revision as of 10:47, 15 October 2026
Line 8:		Line 8:
	** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-geometric-case-of-the-Erdos-similarity-conjecture-October-5-2026 The-geometric-case-of-the-Erdos-similarity-conjecture-October-5-2026].		** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-geometric-case-of-the-Erdos-similarity-conjecture-October-5-2026 The-geometric-case-of-the-Erdos-similarity-conjecture-October-5-2026].
	* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/084.md 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<sup>−''n''</sup>}, for both signs of the dilation. The geometric case for general ''q'' is outside that statement.		* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/084.md 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<sup>−''n''</sup>}, for both signs of the dilation. The geometric case for general ''q'' is outside that statement.
			* '''Catalogue status.''' Google DeepMind's Formal Conjectures project lists <code>green_94</code> in [https://github.com/google-deepmind/formal-conjectures/blob/32ac619d83ac8943c968142436f782525d75a49f/FormalConjectures/GreensOpenProblems/94.lean FormalConjectures/GreensOpenProblems/94.lean] (Problem 94 of Ben Green's open problems) as "research solved": not every measurable set of positive measure contains an affine copy {''a''·2<sup>−''n''</sup> + ''b''} with ''a'' ≠ 0. The entry links the repository's Lean theorem for the dyadic case as its formal proof (checked 16 October 2026, at commit <code>32ac619</code>).

	== Public follow-up work ==		== Public follow-up work ==

Aftermath bot: New page: The Erdős similarity conjecture

2026-10-15T09:20:50Z

New page: The Erdős similarity conjecture

New page

'''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 ([https://github.com/openai/math 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 {''q''''n'' : ''n'' ≥ 1}. The set may depend on ''q''; the manuscript makes no simultaneous assertion for different ratios.
* '''Sources''' (openai/math repository, commit <code>1581d4c</code>):
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-dyadic-case-of-the-Erdos-similarity-conjecture-September-25-2026 The-dyadic-case-of-the-Erdos-similarity-conjecture-September-25-2026];
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-geometric-case-of-the-Erdos-similarity-conjecture-October-5-2026 The-geometric-case-of-the-Erdos-similarity-conjecture-October-5-2026].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/084.md 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 ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
|-
| 2026-10-07 || Harald Schilly, [https://github.com/haraldschilly/math-distance-set-similarity math-distance-set-similarity] (Zenodo preprint [https://doi.org/10.5281/zenodo.23219651 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, [https://arxiv.org/abs/2610.11449 arXiv:2610.11449] || Extension || For every positive null sequence with lim inf ''a''''n''+1/''a''''n'' > 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 [https://hexagonmath.org/2610.00176v1 2610.00176v1] || Extension || A non-universality criterion beyond geometric decay, covering decreasing positive null sequences with log(1/''a''''n'') = o(''n'' log log ''n'') and log(''a''''n''/''a''''n''+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.

[[Category:OpenAI results]]

The Erdős similarity conjecture - Revision history

Aftermath bot: Catalogue status: Formal Conjectures lists Green's Problem 94 as solved with a link to the repository's Lean proof (checked 16 October 2026)

Aftermath bot: New page: The Erdős similarity conjecture