Canonical \(O(3)\) continuum limit and exact \(O(4)\) mass asymptotics
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Constructs the canonical continuum limit of the two-dimensional nearest-neighbor \(O(3)\) model: a non-Gaussian local relativistic theory with a unique vacuum and a positive mass gap. For the square-lattice \(O(4)\) model, determines the exact leading asymptotic of the full transfer gap, \(m_{\mathrm{lat}}(\beta)\sim32e^{\pi/4-1/2}\sqrt\beta\,e^{-\pi\beta}\). The family also proves exponential spin-correlation decay for two-dimensional nearest-neighbor \(O(n)\) models with n ≥ 3 at every positive temperature. (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.
For the nearest-neighbor probability (1.1), the periodic thermodynamic limit \mu_\beta exists for all sufficiently large \beta. Both sums in (1.2) are finite, \chi_\beta,\xi_\beta>0, and \xi_\beta\to\infty as \beta\to\infty. The following limits hold through all real values of \beta tending to infinity.
(i)
For every finite list of vector tests in C_c^\infty(\R^2;\R^3), the fields (1.3) converge jointly in law and in all joint moments to one common limiting hierarchy.
(ii)
For every order and every choice of spin components, the associated Schwinger distributions converge in the strong topology of \mathcal S'((\R^2)^n), that is, uniformly on bounded sets of Schwartz tests.
(iii)
The limiting hierarchy has susceptibility and second-moment length equal to one. It is the hierarchy constructed in Theorem 1.2, after the unique positive constant length and field rescalings imposing these two normalizations.
No Lean statement in the release is paired with this theorem.
Eight more possible matches
Theorem 1.2in The canonical massive continuum limit of the two-dimensional O(3) model, 4 October 2026.
Theorem 1.1in Sharp mass bounds for the two-dimensional O(4) model, 23 September 2026.
Corollary 1.3in The canonical massive continuum limit of the two-dimensional O(3) model, 4 October 2026.
Corollary 1.2(Full gap at every positive temperature)in Sharp mass bounds for the two-dimensional O(4) model, 23 September 2026.
Theorem 1.1in Exact mass asymptotics for the two-dimensional O(4) lattice model, 5 October 2026.
Corollary 1.2(Free-boundary limits)in Exponential decay in two-dimensional classical O(n) models, 23 September 2026.
Theorem 1.1in Exponential decay in two-dimensional classical O(n) models, 23 September 2026.
Theorem 1.1(An isolated lowest mass)in An Isolated Particle Pole for the Two-Dimensional O(3) Spin Field, 4 October 2026.
Reported proof verification
One Lean statement in the release; two independent groups report that Comparator accepted runs for this file at the version shown here.
We construct a canonical interacting massive continuum limit of the two-dimensional nearest-neighbor \(O(3)\) model with unit-length spins, no external field, and no topological term. Normalized by susceptibility and second-moment correlation length, the limit exists as the bare coupling tends to infinity through all positive real values, without selecting subsequences. The limiting fields satisfy the Osterwalder–Schrader axioms and have a nonzero connected four-point correlation on separated time supports. Their reconstructed theory has a unique vacuum, a nonzero vacuum complement, and a positive Hamiltonian gap on that entire complement.
We consider the continuum spin field constructed from the nearest-neighbor two-dimensional \(O(3)\) model by the fixed prescription of the companion paper. We prove that its vector two-point spectral measure has a positive atom corresponding to the lowest mass, separated by a positive gap from all remaining mass support.
For the nearest-neighbor \(O(4)\) model on the square lattice at inverse temperature β, we prove the exact low-temperature asymptotic \(\displaystyle m_{\mathrm{lat}}(\beta)\sim 32\exp(\pi/4-1/2)\sqrt\beta\,\exp(-\pi\beta) \qquad (\beta\to\infty).\) Here the mass is the gap of the full Osterwalder–Schrader transfer operator, including rotation-invariant local-observable sectors, in units of one original lattice time step.
We prove sharp mass bounds for the two-dimensional nearest-neighbor \(O(4)\) model. For all sufficiently large inverse couplings β, the full transfer gap, including rotation-invariant local-observable sectors, is bounded above and below by positive multiples of \(\sqrt\beta e^{-\pi\beta}\). We also prove that the model has a unique periodic local limit and a positive full gap at every finite β > 0, resolving the all-temperature lattice mass-generation conjecture for this periodic state. Under the stated cutoff scaling, the mass bounds are uniform in independently fixed physical units. A continuum spectral interpretation requires separate convergence hypotheses for the transfer semigroup and the block observables.
We prove exponential decay of two-point correlations for the classical nearest-neighbor \(O(n)\) model on the square lattice, for every n ≥ 3 and every finite positive inverse temperature. The estimate is uniform over finite free-boundary subgraphs and bounded nonnegative edge strengths. This resolves positively the all-temperature exponential spin-decay conjecture for these models.
One Lean statement in this family
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.
For every integer n\ge3 and every finite \beta>0, there are constants A=A(n,\beta)<\infty and m=m(n,\beta)>0 such that, for every finite nearest-neighbor square-lattice subgraph G, every strength array b\in[0,\beta]^E, and all x,y\in V,
ClassicalON.lean, the release lists it as a main result.
defExponentialDecay : Prop := ∀ (n : ℕ), 3 ≤ n → ∀ (β : ℝ), 0 < β → ∃ A m : ℝ, 0 < m ∧ ∀ (G : LatticeGraph) (b : G.edges → ℝ), (∀ e, 0 ≤ b e ∧ b e ≤ β) → ∀ x y : G.vertices,0 ≤ correlation n G b x y ∧ correlation n G b x y ≤ A * Real.exp (-m * siteDistance x.val y.val)⋮theoremmain : ExponentialDecay := 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.
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:PRIMARY CLAIM NOT STATED (only a secondary result is formalized). Only exponential decay of spin correlations is stated: ExponentialDecay : ∀ n ≥ 3, ∀ β > 0, ∃ A m, 0 < m ∧ ∀ finite lattice graph G, b ∈ [0,β] → 0 ≤ correlation ≤ A * exp(-m * siteDistance x y) (free boundary, finite volume, uniform in the graph; docs: 'The infinite-volume limit and the separate O(4) spectral-gap claim are not included'). The summary’s headline results, the canonical O(3) continuum limit with positive mass gap and the exact O(4) asymptotic m_lat(β) ~ 32 e^{π/4-1/2} √β e^{-πβ}, are not stated.
“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 O(3) canonical continuum limit (undeclared) and the O(4) exact mass asymptotic (declared)
“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.
The formalized result proves exponential decay of spin correlations for the two-dimensional classical $O(n)$ model at every temperature when $n\ge3$. For each interaction bound $\beta>0$, constants $A$ and $m>0$ work for every finite square-lattice subgraph with free boundary and nonnegative edge strengths at most $\beta$: the correlation between sites $x,y$ is at most $Ae^{-m|x-y|}$. The infinite-volume limit and the separate $O(4)$ spectral-gap claim are not included.
AI-drafted comparisons, with no recorded human review
Exponential correlation decay for classical $O(n)$ modelsClassicalON
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: exponential decay of spin correlations in the two-dimensional O(n) model, n ≥ 3, at every temperature, uniformly over finite subgraphs with free boundary. The infinite-volume corollary is not included.
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.
Exponential correlation decay for classical $O(n)$ modelsClassicalON
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.
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 “Would win a Fields Medal”. The page says that nothing on it is verified.
Scientific American (byline not recorded), The most exciting claims from OpenAI’s heap of new proofs, 8 October 2026. Source
Roland Bauerschmidt (NYU) calls the first of OpenAI’s sigma-model papers groundbreaking and comprehensible but finds the others too hard for human experts to verify; Michael Douglas (Harvard) describes the problem as the long-standing warm-up for Yang-Mills.
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.
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
Identify the theorem the catalogue describes
Family 215The 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
Compare the proposed paper and Lean matches
Family 215Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing.Open the form
Why this passage is shown
Theorem 1.1 (Canonical continuum limit)
In The canonical massive continuum limit of the two-dimensional O(3) model, 4 October 2026
How it was found
Its words were compared with the words of OpenAI’s catalogue description.
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; 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; 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.