OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Proves the spin-one Haldane gap conjecture for the pure antiferromagnetic Heisenberg chain on even periodic rings: the spectral gap stays uniformly positive as the chain grows. A companion establishes a gap for odd open chains with endpoint field \(h=3/5\) and gives boundary-selected infinite-volume states with topological index −1.
The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
For the Hamiltonians (1.1), the ground state is unique for every even L\ge60, and
\begin{aligned}\gamma_L&>\frac4{105}\log\frac{80}{79}
&&\text{for every even }L\ge60,\\
\gamma_L&>\frac{\log20}{784}
&&\text{for every even }L\ge2304.\end{aligned}
Consequently
\Delta_1\ge\frac{\log20}{784}>0.
The spectral conclusions also hold for any simultaneously similar spin-one realization satisfying the same commutator and Casimir normalizations.
The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.
For the Hamiltonian (1.1), with the spin normalization above,
E_1(L,3/5)-E_0(L,3/5)>\frac{\log 10}{392}
\qquad\text{for every integer }L\ge960.
The release does not say which paper theorem its catalogue describes. Both statements above are shown whole, the closer match to the description’s wording first. The atlas has not reviewed either choice.
Reported proof verification
The release has no Lean statement for this family. The papers are available to read and assess.
We prove a uniform positive spectral gap for the pure antiferromagnetic spin-one Heisenberg chain on even periodic rings, establishing the positive even-periodic formulation of the spin-one Haldane conjecture.
We prove a uniform spectral gap for odd open spin-one antiferromagnetic Heisenberg chains with the same fixed magnetic field at both endpoints. The field \(h=3/5\) gives a gap greater than \(\log(10)/392\) on every chain of \(2L+1\) sites with L ≥ 960. Tasaki’s index theorem then gives index −1 for every subsequential local limit of these boundary-selected ground states.
Lean statements
The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.
Other proofs and exact calculations
These reports examine claims in the papers using exact calculations for finite claims, independently of the release’s Lean proofs. Read each report for the exact claim it covers.
“CERTIFIED” Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: the finite inputs of the two initializations — the trial MPS contractions at N = 72, 120 (exact U_N, V_N), the thermal recurrences (all nine t_{n,g} at b = 21/2 and W_{n,g} at b = 49/4 for n <= 12 recomputed exactly, all 27 rational enclosures), and every scalar comparison of prop:seed60, prop:seed2304 and the bootstrap parameters. NOT the gap theorem: the transfer operator, sector decomposition, purity bootstrap, filter/capped-mass lemmas, Fox-Glynn and Horner error arguments and the variational principle are analytic and outside this check”
“CERTIFIED” Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: the fifteen thermal integers k_{n,g} recomputed by the printed recurrence and every enclosure built on them (Y_6 < .027, c_0 P_*(lambda_0)^2 < .003745), the four trial-vector certificates (m = 34, 78, 142, 240) recomputed exactly, and every printed scalar comparison of the initialization, periodic extraction and conclusion. NOT the gap theorem: the boundary transfer identity, the averaging identity, the boundary recurrence lemmas, the purity lemma and the variational principle are analytic; the periodic inputs are the companion’s (F-539), used here as printed”
Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.
seaworld008, seaworld008/openai-math-top30: thirty selected families explained in Chinese, 7 October 2026. Source
Chinese-language explainer for general readers, with a beginner’s section, a specialist section, background on why the problem was hard and a diagram; it ends by saying it paraphrases OpenAI’s summary and does not represent consensus.
Yixin Ma, OpenAI mathematical physics, 25 families: a Chinese guided reading, 7 October 2026. Source
Chinese guided reading of this family that compares the manuscripts’ main theorems with their abstracts and flags boundary conditions and limit orders that change the physical reading; drafted with Codex and not a re-proof.
What these papers cite in the release, and what cites them
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.
Papers elsewhere in the release that this family’s papers cite
This family’s papers cite no paper elsewhere in the release.
Papers elsewhere in the release that cite this family’s papers
No paper elsewhere in the release cites this family’s papers.
References outside the release
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
Explain a result, compare statements or propose a correction
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.
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 proof and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
Isaac Kim, Post listing quantum information results in the release, 6 October 2026. Source
Names the spin-one Haldane gap.
Questions awaiting review
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Identify the theorem the catalogue describes
Family 268The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.Open the form
State the result in Lean
Family 268The release has no Lean statement for this family.Open the form
Why this passage is shown
Theorem 1.1
In The periodic spin-one Haldane gap, 24 September 2026
How it was found
Its words were compared with the words of OpenAI’s catalogue description.
Words they share
even, spectral, spin
Review
Atlas records no review confirming that this is the theorem OpenAI’s description refers to.
Exact calculations for finite claims, cert-machine
Their verdict
“CERTIFIED”
Claim tested or proved
Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: the finite inputs of the two initializations — the trial MPS contractions at N = 72, 120 (exact U_N, V_N), the thermal recurrences (all nine t_{n,g} at b = 21/2 and W_{n,g} at b = 49/4 for n <= 12 recomputed exactly, all 27 rational enclosures), and every scalar comparison of prop:seed60, prop:seed2304 and the bootstrap parameters. NOT the gap theorem: the transfer operator, sector decomposition, purity bootstrap, filter/capped-mass lemmas, Fox-Glynn and Horner error arguments and the variational principle are analytic and outside this check”
Exact calculations for finite claims, cert-machine
Their verdict
“CERTIFIED”
Claim tested or proved
Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: the fifteen thermal integers k_{n,g} recomputed by the printed recurrence and every enclosure built on them (Y_6 < .027, c_0 P_*(lambda_0)^2 < .003745), the four trial-vector certificates (m = 34, 78, 142, 240) recomputed exactly, and every printed scalar comparison of the initialization, periodic extraction and conclusion. NOT the gap theorem: the boundary transfer identity, the averaging identity, the boundary recurrence lemmas, the purity lemma and the variational principle are analytic; the periodic inputs are the companion’s (F-539), used here as printed”