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. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement. Read the assessments
It bears on Erdős problem #120, as listed by Thomas Bloom, erdosproblems.com.
In The dyadic case of the Erdős similarity conjecture, 25 September 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
For every \eta\in(0,1), there is a compact set E_\eta\subseteq[0,1] with m(E_\eta)>1-\eta such that
Equivalently, for every such x,s there is an integer n\ge1 with x+s2^{-n}\notin E_\eta.
In The geometric case of the Erdős similarity conjecture, 5 October 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
For every q\in(0,1) and \eta\in(0,1), there is a compact set E_{q,\eta}\subseteq[0,1] with m(E_{q,\eta})>1-\eta such that
No Lean statement in the release is paired with this theorem.
The release does not say which paper theorem its catalogue describes. The statements above share the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.
Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.
Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
DyadicAvoidanceThe paper states
In The dyadic case of the Erdős similarity conjecture, 25 September 2026
For every \eta\in(0,1), there is a compact set E_\eta\subseteq[0,1] with m(E_\eta)>1-\eta such that
Equivalently, for every such x,s there is an integer n\ge1 with x+s2^{-n}\notin E_\eta.
The words they share: compact, integer, dyadic, eta.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
DyadicAvoidance.lean, the release lists it as a supporting statement.
theorem dyadic_affine_avoidance : ∀ η : ℝ, 0 < η → η < 1 → ∃ E : Set ℝ, E ⊆ Set.Icc (0 : ℝ) 1 ∧ IsCompact E ∧ MeasureTheory.volume E > ENNReal.ofReal (1 - η) ∧ ∀ x s : ℝ, s ≠ 0 → ∃ n : ℕ, 1 ≤ n ∧ x + s * dyadicPoint n ∉ E := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express part of the advertised result (their term: “partial”).
Their note: Only q = 1/2 (dyadic) is stated; the geometric-progression case for every ratio q in (0,1) is not.
“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).
The gap they name: The headline claims every ratio q ∈ (0,1); the Lean states only q = 1/2. The general-ratio theorem is the October 5 manuscript (‘The geometric case…’), which the scope note does not link.
“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
OpenAI’s own note on what its Lean covers
The formalization proves the dyadic case of the Erdős similarity conjecture. For every $0<\eta<1$, it constructs a compact set $E\subset[0,1]$ of measure greater than $1-\eta$ that contains no affine copy of $\{2^{-n}:n\ge1\}$. Explicitly, for every translation $x$ and every nonzero real dilation $s$, some point $x+s2^{-n}$ lies outside $E$. Both signs of $s$ are included.
Positive-measure avoidance of every affine dyadic sequence DyadicAvoidance
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: for every η in (0, 1) a compact subset of [0, 1] of measure above 1 − η containing no affine copy of {2^{-n}}. The geometric case of the family’s later paper is not part of the statement.
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
DyadicAvoidanceThree reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 136 s). | 10 October 2026 | Original report |
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
This family’s papers cite no paper elsewhere in the release.
No paper elsewhere in the release cites this family’s papers.
Hexagon, Hexagon: a repository for research in the mathematical sciences and theoretical computer science, 9 October 2026. Source
hexagon:2610.00176v1 (Vjekoslav Kovač, text from ChatGPT 6 Astra on 9 October) proves a non-universality criterion for the Erdős similarity conjecture beyond geometric decay, building on OpenAI’s geometric-case manuscript.
Harald Schilly, haraldschilly/math-distance-set-similarity: Erdős similarity for distance sets in Lean 4, 7 October 2026. Source
Erdős similarity result for distance sets formalised in Lean on top of OpenAI’s libraries.
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Offer to write an explanationCompare the Lean statement with the paperSuggest a source attributionSuggest a change
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a counterexample and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.
Author not stated. Source
Moritz Firsching, anxkhn, Paul Lezeau, Formal Conjectures: mark problems solved in the OpenAI math release and link formal proofs, 11 October 2026. Source
A Formal Conjectures maintainer, after source inspection, links the dyadic avoidance result to Green’s problem 94.
Thomas Bloom, Erdős problems in the OpenAI proofs, 8 October 2026. Source
Bloom lists Erdős 120 (the similarity problem for geometric sequences) and notes the Lean covers only the ratio one half.
Kan Jiang, Lifeng Xi, The Erdős similarity problem for null sequences with adjacent ratios bounded below, 8 October 2026. Source
Jiang and Xi cite OpenAI’s dyadic and geometric cases of the Erdos similarity conjecture as the nearest results to their theorem on null sequences with adjacent ratios bounded below.
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Why this passage is shown
Theorem 1.1
In The dyadic case of the Erdős similarity conjecture, 25 September 2026
Why this passage is shown
Theorem 1.1
In The geometric case of the Erdős similarity conjecture, 5 October 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, DyadicAvoidance
Proof-verification report
MathVet, DyadicAvoidance
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, DyadicAvoidance
Lean statement
DyadicAvoidance