Proves that QAOA approaches the ground-state energy of the Gaussian zero-field Sherrington–Kirkpatrick model when system size tends to infinity before circuit depth. For every accuracy, finite depth and deterministic angles independent of size and disorder achieve the required limiting expected energy per spin. This also yields leading-order optimal expected MaxCut values on large-degree random regular graphs, with size tending to infinity before degree. (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 a supporting step or a different result. Read the assessments
In QAOA attains the SK ground-state energy in the thermodynamic-first limit, 25 September 2026
The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.
For the zero-field SK model (1.1),
Equivalently, for every \varepsilon>0 there exist a finite integer p and deterministic real vectors \gamma,\beta\in\R^p, independent of n and J, such that v_p(\gamma,\beta)\ge\Pstar-\varepsilon.
In QAOA attains the SK ground-state energy in the thermodynamic-first limit, 25 September 2026
Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.
For every \eta>0 there are an integer p\ge1, deterministic normalized angles \gamma,\beta\in\R^p, and an integer D_0\ge2 such that, for every integer D\ge D_0 and every finite simple unweighted (D+1)-regular graph G of girth greater than 2p+1,
The word p,\gamma,\beta is independent of D, the graph size, and G; the displayed usual MaxCut cost angles, unlike the normalized angles \gamma, are scaled with the degree.
Let G_{n,d} be uniform among simple labelled d-regular graphs on n vertices, along admissible n with nd even. For the same word, put
The word may be chosen so that
Here the inner limit keeps D,p,\gamma,\beta fixed, and \Pr_G is only over the graph: q_{p,G} already averages quantum measurement.
No Lean statement in the release is paired with this theorem.
The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.
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.
Choose one to see it beside the paper theorem it is paired with. The outside readers find that the release’s Lean states a supporting or different result, so the theorem it is paired with is shown under its own heading.
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.
SKFullSupportThe paper states
In Full support of the zero-temperature Sherrington-Kirkpatrick order parameter, 27 September 2026
If \gamma\in\mathcal U minimizes \mathcal P, then
In particular \gamma(b)>\gamma(a) whenever 0\leq a<b<1. For the solution of (1.5),
The words they share: support, full, diffusion, order, parameter, temperature, model, zero.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
SKFullSupport.lean, the release lists it as a supporting statement.
theorem full_support (W : BrownianSystem Ω) (γ : OrderParameter) (hmin : IsMinimizer W γ) : FullSupportConclusion W γ := 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.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program
SKValueThe paper states
In QAOA attains the SK ground-state energy in the thermodynamic-first limit, 25 September 2026
For the zero-field SK model (1.1),
Equivalently, for every \varepsilon>0 there exist a finite integer p and deterministic real vectors \gamma,\beta\in\R^p, independent of n and J, such that v_p(\gamma,\beta)\ge\Pstar-\varepsilon.
The words they share: equivalently, field, finite, model, zero.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
SKValue.lean, the release lists it as a supporting statement.
theorem value_consequences : (∀ (W : BrownianSpace) (γ : OrderParameter) (X : ℝ → W.Ω → ℝ), IsMinimizer W γ → IsDiffusion W γ X → ScalarValueConclusion W γ X) ∧ (∀ (W : BrownianSpace) (γ : OrderParameter) (X : ℝ → W.Ω → ℝ) (T : ℝ), 0 < T → T < 1 → IsMinimizer W γ → IsDiffusion W γ X → FiniteGaussianConclusion W γ X T) ∧ (∀ (W : BrownianSpace) (γ : OrderParameter), IsMinimizer W γ → groundStateValue = parisi W γ) := 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.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program
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.
IsMinimizer Model.lean, line 62IsStieltjesMeasure Model.lean, line 65IsDiffusion Model.lean, line 68FullSupportConclusion Model.lean, line 81Admissible Model.lean, line 59IsMinimizer Model.lean, line 80IsDiffusion Model.lean, line 83ScalarValueConclusion Model.lean, line 106FiniteGaussianConclusion Model.lean, line 155Neither 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 a supporting result (their term: “supporting-only”).
Their note: No QAOA statement exists. The challenges are SKValue.value_consequences (conditional on IsMinimizer W γ and a diffusion X: the finite-size SK ground-state energy per spin groundStateSequence n converges to groundStateValue = parisi W γ, with martingale/curvature-integral formulas and convergence of finite Gaussian coefficient sums) and SKFullSupport.full_support (full support of zero-temperature Parisi minimizers). Docs: ‘it does not itself assert convergence of QAOA circuit energies’, and ‘does not separately assert existence of a minimizer’. The summary’s headline (QAOA with finite depth and size/disorder-independent angles reaches the SK ground-state energy per spin, size before depth, plus MaxCut on random regular graphs) is absent.
Definitions the group asks readers to compare with the paper: Custom Parisi/stochastic-control objects: phi W γ t x := sSup {controlPayoff..} over Admissible progressive controls (real sSup), gradient := deriv (phi W γ t), curvature := deriv (gradient..), parisi, IsMinimizer, groundStateValue := limUnder atTop groundStateSequence (convergence asserted in ScalarValueConclusion); derivatives are Mathlib deriv (junk 0 where not differentiable).
“supporting-only”, in their words: The challenge statements state a lemma or auxiliary result, not the headline.
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 different result (their term: “DIFFERENT”).
The gap they name: The whole headline. The challenges state (i) value identities for the zero-temperature SK model conditional on a Parisi minimizer and its diffusion — convergence of the finite-n ground-state energy, equality with the Parisi value, terminal-martingale and integrated-curvature formulas, convergence of finite Gaussian coefficient sums — and (ii) full support of every zero-temperature Parisi minimizer. These are ingredients of the QAOA argument; none mentions QAOA.
“DIFFERENT”, in their words: The challenge statements state a different theorem from the headline.
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 linked formalization supplies variational identities for the Gaussian zero-field Sherrington–Kirkpatrick ground-state energy used in the paper’s QAOA argument. Conditional on an admissible Parisi minimizer and its associated diffusion, it proves convergence of the finite-system ground-state energy, identifies its limit with the Parisi value, and gives equivalent terminal-martingale and integrated-curvature formulas.
It also proves convergence of finite Gaussian coefficient sums to the curvature integral, which approaches the ground-state value as the terminal time tends to one. The selected statement covers these value and approximation results; it does not itself assert convergence of QAOA circuit energies. The formalization proves that every admissible integrable minimizer of the zero-temperature Parisi functional for the pure zero-field Sherrington–Kirkpatrick model has full relative Stieltjes support on $[0,1)$. Equivalently, the order parameter increases strictly between every two overlap values below one, so its support has no gap. The covariance normalization is $\xi(t)=t^2/2$. The statement also constructs the associated diffusion and proves its selected self-consistency moment identities. It is conditional on the order parameter being a minimizer and does not separately assert existence of a minimizer.
Full support of zero-temperature SK minimizers SKFullSupport
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the full-support paper: every admissible minimiser of the zero-temperature Parisi functional has support [0, 1), with the associated diffusion and moment identities.
Parisi ground-state value identities and finite Gaussian approximation SKValue
Unreviewed AI draft: states a supporting result. States variational identities for the SK ground-state energy used in the QAOA argument, conditional on an admissible Parisi minimiser. It does not assert convergence of QAOA energies, the main theorem.
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.
SKFullSupportTwo 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 |
SKValueTwo 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 |
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.
Lemmas 4.1 and 3.4 of Full support of the zero-temperature Sherrington-Kirkpatrick order parameter, 27 September 2026
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.
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.
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 one Lean statement with its paper: SKValue, SKFullSupportSuggest 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 proof and rates its significance, if it holds up, as “Solid publication, could lead to tenure”. The page says that nothing on it is verified.
Author not stated. Source
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 QAOA attains the SK ground-state energy in the thermodynamic-first limit, 25 September 2026
Why this passage is shown
Corollary 1.2 (Regular MaxCut in successive limits)
In QAOA attains the SK ground-state energy in the thermodynamic-first limit, 25 September 2026
Why this passage is shown
Theorem 1.1 (Full support at zero temperature)
In Full support of the zero-temperature Sherrington-Kirkpatrick order parameter, 27 September 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, SKFullSupport
Proof-verification report
MathVet, SKFullSupport
Proof-verification report
cert-machine, SKValue
Proof-verification report
MathVet, SKValue
Report using another proof or calculation method
Lemmas 4.1 and 3.4 of Full support of the zero-temperature Sherrington-Kirkpatrick order parameter, 27 September 2026
Exact calculations for finite claims, cert-machine
9814e4cLean statement
SKFullSupport
Lean statement
SKValue