Uniform Laughlin gap and stability under bounded scalar disorder
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Proves the fermionic Laughlin spectral-gap conjecture for the full V1 interaction at filling 1/3 on the round sphere. The unique ground state remains uniformly gapped under sufficiently weak bounded real scalar one-body potentials projected to the lowest Landau level. Both the gap and disorder threshold are uniform over all sufficiently large particle numbers and all normalized potential profiles. (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
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.
The other possible matches are Theorem 1.1 in A Fock-space inequality and the Laughlin spectral gap () and Corollary 1.2 in A Fock-space inequality and the Laughlin spectral gap ().
There are constants \lambda_*>0,\Delta_*>0, and N_*<\infty such that, for every N\ge N_*, every real bounded measurable \varphi on S_{3(N-1)} with \|\varphi\|_\infty\le1, and every real |\lambda|\le\lambda_*,
We prove that the fermionic Laughlin V1 Hamiltonian at filling 1/3 on expanding round spheres retains a unique ground state and a uniform spectral gap under sufficiently weak bounded real scalar one-body potentials projected to the lowest Landau level. With coefficient one for each pair projector and Laughlin flux \(q=3(N-1)\), the gap and perturbation threshold are uniform for all sufficiently large particle numbers and all potential profiles of supremum norm at most one. The result uses the uniform unperturbed Fock-space gap and gives existential constants.
We prove the spherical fermionic Laughlin spectral-gap conjecture for the full V1 interaction. With coefficient one for each pair projector, the gap above the Laughlin state at filling 1/3 on the round sphere is at least 1/25 for all sufficiently large systems. More generally, \(H_Q^2\ge\gamma H_Q\) for some fixed \(\gamma\gt 1/25\) on the entire lowest-Landau-level Fock space for all sufficiently large flux Q, independently of particle number.
Four Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
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.
Laughlin
The paper states
No paper theorem is paired with this Lean statement.
no paper statement matches the Lean text clearly enough to pair, so the closest candidates are listed below.
Statements it shares words with:
Corollary 7.1(Planar spectral gap)in A Fock-space inequality and the Laughlin spectral gap, 24 September 2026.
Theorem 6.6(Local expectations are linear in the number of holes)in Uniform Stability of the Spherical Laughlin Gap, 5 October 2026.
Corollary 6.3(Charge versus neutral gap at fixed flux)in A Fock-space inequality and the Laughlin spectral gap, 24 September 2026.
Theorem 1.1(Uniform scalar-disorder stability)in Uniform Stability of the Spherical Laughlin Gap, 5 October 2026.
Theorem 1.1in A Fock-space inequality and the Laughlin spectral gap, 24 September 2026.
Proposition 5.3(Four-body estimate)in A Fock-space inequality and the Laughlin spectral gap, 24 September 2026.
Corollary 4.6(Cost of changing a calibration state)in Uniform Stability of the Spherical Laughlin Gap, 5 October 2026.
Corollary 1.2in A Fock-space inequality and the Laughlin spectral gap, 24 September 2026.
Laughlin.lean, the release lists it as a main result.
defMainTarget : Prop := ∃ N₀ : ℕ, 2 ≤ N₀ ∧ ∀ N : ℕ, N₀ ≤ N → ∀ ψ : State N (3*(N-1)), Antisymmetric ψ → (1/100 : ℝ) * distanceToLaughlinSq ψ ≤ energy ψ⋮theoremmainTarget_proved : MainTarget := bysorry
This 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.
This 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.
There are constants \lambda_*>0,\Delta_*>0, and N_*<\infty such that, for every N\ge N_*, every real bounded measurable \varphi on S_{3(N-1)} with \|\varphi\|_\infty\le1, and every real |\lambda|\le\lambda_*,
LaughlinGap.lean, the release lists it as a supporting statement.
defMainTarget : Prop := ∃ N₀ : ℕ, 2 ≤ N₀ ∧ ∀ N : ℕ, N₀ ≤ N → ∀ ψ : State N (3*(N-1)), Antisymmetric ψ → (1/25 : ℝ) * distanceToLaughlinSq ψ ≤ energy ψ⋮theoremthm_main : MainTarget := bysorry
This 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.
This 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.
Other mathematical statements in OpenAI’s Lean library
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
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:Stated: the unperturbed spherical Laughlin gap at flux Q = 3(N-1): Laughlin.MainTarget (1/100) and LaughlinGap.MainTarget ((1/25) * distanceToLaughlinSq ψ ≤ energy ψ for every antisymmetric ψ and N >= N₀), the Fock-space inequality thm_fock (H² ≥ γ H for all γ < γ* ≈ 0.4617 and large flux, independent of particle number) and a planar version. Not stated: the summary’s second claim, stability of the uniform gap and uniqueness of the ground state under weak bounded real scalar one-body potentials projected to the lowest Landau level (docs: 'Stability under projected one-body potentials and uniqueness of the perturbed ground state are outside it'); nor that laughlinVector is a zero-energy state (the inequality is stated against the line through it).
Definitions the group asks readers to compare with the paper:Hand-coded spherical V₁ Hamiltonian: energy ψ := Σ_{i<j} Σ_{p<2Q-1} Σ_{a, a_i = a_j = 0} |pairAmplitude ψ i j p a|² with explicit Clebsch-Gordan-type pairCoefficient Q p x y (descFactorial/factorial formula), laughlinVector from the coefficients of ∏(z_i w_j - z_j w_i)^3, and distanceToLaughlinSq ψ := sInf (range (c ↦ ‖ψ - c • laughlin‖²)). Its agreement with the physical V₁ projector is not machine-checked against any standard definition.
“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 — DECLARED”).
The gap they name:Stability of the gap and uniqueness of the ground state under projected bounded scalar one-body potentials (the October 5 ‘Uniform Stability’ result).
“NARROWER — DECLARED”, in their words: The challenge statements state less than the headline, and OpenAI’s Lean note says so.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
The linked formalization proves the uniform unperturbed gap estimate used in the paper’s stability argument for the fermionic Laughlin state at filling $1/3$ on the sphere. At flux $q=3(N-1)$ and all sufficiently large particle numbers $N$, every antisymmetric state has $V_1$ energy at least $1/25$ times its squared distance from the Laughlin ground-state line.
This selected statement is the unperturbed Fock-space inequality. Stability under projected one-body potentials and uniqueness of the perturbed ground state are outside it.
The Laughlin spectral-gap problem asks for a positive gap that remains uniform as the system grows. The formalization includes the finite spherical $V_1$ bound of $1/100$ above the Laughlin state at flux $3(N-1)$ for all sufficiently large particle numbers $N$. It also proves the stronger Fock-space inequality $H_Q^2\ge\gamma H_Q$ for every fixed $0<\gamma<\gamma_*$ and all sufficiently large fluxes $Q$, independently of particle number, where $\gamma_*=4616733319001/10^{14}>1/25$.
For the untruncated planar model, the formalization proves the corresponding inequality at the endpoint $\gamma_*$ on every homogeneous particle sector. These statements use coefficient one for each pair projector.
AI-drafted comparisons, with no recorded human review
Uniform Laughlin $V_1$ spectral gapLaughlin
Unreviewed AI draft: states a weaker form of a paper’s theorem. States a uniform V₁ gap of 1/100 above the Laughlin state at flux 3(N − 1), whereas the paper’s corollary gives 1/25; the Fock-space theorem itself is LaughlinFock.
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the Fock-space paper: H_Q² ≥ γH_Q for every γ < γ* and all large Q, independently of particle number.
Uniform unperturbed spherical Laughlin gap inequalityLaughlinGap
Unreviewed AI draft: states a supporting result. States the unperturbed gap inequality (V₁ energy at least 1/25 of the squared distance to the Laughlin line) that the stability paper uses as input; it coincides with the companion paper’s corollary. Stability under disorder, the stability paper’s main theorem, is outside it.
Planar spectral-gap inequalityLaughlinPlanar
Unreviewed AI draft: states a consequence of a paper’s theorem. States the paper’s planar corollary: the untruncated planar Hamiltonian satisfies the inequality at the endpoint γ* on every homogeneous sector.
Who ran the proof-verification program?
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.
Uniform Laughlin $V_1$ spectral gapLaughlin
Two 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.
Other people’s accounts of running proof-verification software, with links to their reports.
carlostoledo1891, def_eq unfolds proofs when proof irrelevance fails (issue 44), with a replay of every openai/math challenge, 11 October 2026. Source
Laughlin, LaughlinFock and LaughlinPlanar are accepted by nanoda with the patch on the stock stack (6.8 to 8.5 GB peak, 33 to 142 minutes).
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: this paper’s restated seven-row certificate (Appendix A) — 13 three-body margins > 0 with the printed floors, M >= 0 exactly for D = 1..23 with the printed sign table, P^2 eta, 61/4096, 1222 and the final margin 4616733319001/10^14 > 1/25 used for 0 < c_0 < 1/25. NOT the stability theorem: its constants lambda_*, Delta_*, N_* are existential and every analytic step is 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 seven published rows give the 13 three-body margins of eq:3certificate (all > 0, floors as printed) and the 23 four-body certificates of eq:4certificate (M >= 0 exactly, sign table as printed), each re-derived from the definitions and from the paper’s rational formulas; plus P^2 eta, 61/4096, 1222 and gamma_* = 4616733319001/10^14 > 1/25. NOT the analytic reduction from these certificates to H_Q^2 >= gamma H_Q or to the 1/25 gap (lemmas, limits, transfer, tail, existential Q_gamma and N_0).”
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 “Major math journal”. The page says that nothing on it is verified.
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Read the Lean statement against the paper
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
Identify the theorem the catalogue describes
Family 269The 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
Address a question raised in an independent assessment
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Theorem 1.1
In A Fock-space inequality and the Laughlin spectral gap, 24 September 2026
How it was found
Its words were compared with the words of the Lean statement LaughlinPlanar.
Words they share
gamma, integer, particle, number, inequality, gap, space
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Corollary 1.2
In A Fock-space inequality and the Laughlin spectral gap, 24 September 2026
How it was found
Its words were compared with the words of the Lean statement LaughlinPlanar.
Words they share
integer, inequality, gap, space
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Corollary 6.3 (Charge versus neutral gap at fixed flux)
In A Fock-space inequality and the Laughlin spectral gap, 24 September 2026
How it was found
Its words were compared with the words of the Lean statement LaughlinPlanar.
Words they share
coefficient, gap, particle, number, one
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition A.1 (Retained four-body blocks)
In Uniform Stability of the Spherical Laughlin Gap, 5 October 2026
How it was found
Its words were compared with the words of the Lean statement LaughlinPlanar.
Words they share
blocks, inequality, integer, particle, space, number
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Theorem 1.1 (Uniform scalar-disorder stability)
In Uniform Stability of the Spherical Laughlin Gap, 5 October 2026
How it was found
Its words were compared with the words of the Lean statement LaughlinPlanar.
Words they share
real, state, gap
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition 7.4 (Control of particle number)
In Uniform Stability of the Spherical Laughlin Gap, 5 October 2026
How it was found
Its words were compared with the words of the Lean statement LaughlinPlanar.
Words they share
limit, matrix, particle, number, sectors
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Theorem 2.2 (Uniform unperturbed gap)
In Uniform Stability of the Spherical Laughlin Gap, 5 October 2026
How it was found
Its words were compared with the words of the Lean statement LaughlinPlanar.
Words they share
4616733319001/10, gamma, gap
Review
Atlas records no review confirming that the two statements mean the same thing.
Independent assessment
MathVet
Their term
“partial”
What their term means
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. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state less than the headline, and OpenAI’s Lean note says so.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
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: this paper’s restated seven-row certificate (Appendix A) — 13 three-body margins > 0 with the printed floors, M >= 0 exactly for D = 1..23 with the printed sign table, P^2 eta, 61/4096, 1222 and the final margin 4616733319001/10^14 > 1/25 used for 0 < c_0 < 1/25. NOT the stability theorem: its constants lambda_*, Delta_*, N_* are existential and every analytic step is 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 seven published rows give the 13 three-body margins of eq:3certificate (all > 0, floors as printed) and the 23 four-body certificates of eq:4certificate (M >= 0 exactly, sign table as printed), each re-derived from the definitions and from the paper’s rational formulas; plus P^2 eta, 61/4096, 1222 and gamma_* = 4616733319001/10^14 > 1/25. NOT the analytic reduction from these certificates to H_Q^2 >= gamma H_Q or to the 1/25 gap (lemmas, limits, transfer, tail, existential Q_gamma and N_0).”