OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Proves Saxl’s conjecture: the tensor square of every staircase representation contains every irreducible complex representation of the corresponding symmetric group. More generally, every Sn with \(n\notin\{2,4,9\}\) has an irreducible representation whose tensor square contains all irreducibles. (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.
Both independent assessments find that the Lean statements express or imply the whole result described above.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 Universal Tensor Squares for Symmetric Groups () and Corollary 1.2(Unipotent tensor squares) in Universal Tensor Squares for Symmetric Groups ().
For every integer m\ge1 and every partition \lambda\vdash N_m,
g(\rho_m,\rho_m,\lambda)>0.
Equivalently, S^{\rho_m}\otimes S^{\rho_m} contains every irreducible complex representation of S_{N_m}.
Reported proof verification
Two Lean statements in the release; three independent groups report that Comparator accepted runs for one statement file at the version shown here.
For every positive integer n other than 2, 4, and 9, we prove that some irreducible complex representation of Sn has a tensor square containing every irreducible representation. This resolves the tensor square conjecture for symmetric groups affirmatively.
For every staircase partition, we prove that the tensor square of the corresponding irreducible complex representation of the symmetric group contains every irreducible representation of that group. This proves Saxl’s conjecture.
Two 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.
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.
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
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
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.
Atlas has no report of an independent group using Comparator to verify OpenAI’s proof of this Lean statement at the version shown here. Who ran the proof-verification program
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?
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
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 or imply the whole advertised result (their term: “full”).
Their note:Saxl.saxl_conjecture : ∀ m ≥ 1, ∀ μ with μ.card = (staircase m).card, 0 < kronecker (staircase m) (staircase m) μ and universal_tensor_square (n) (hn : 0 < n) (h2 : n ≠ 2) (h4 : n ≠ 4) (h9 : n ≠ 9) : ∃ λ, (∀ ν, 0 < kronecker λ λ ν) ∧ IsIrreducible (spechtRep λ) ∧ ∀ irreducible ρ, ∃ injective intertwiner ρ → S^λ ⊗ S^λ. Both summary claims are stated.
Definitions the group asks readers to compare with the paper:Specht modules are hand-built: spechtSub t := cyclic (wordRep n d) (polytabloid t) as the orbit span of the column-antisymmetrized row-word inside (Fin n → Fin d) → ℂ, and kronecker := finrank ℂ (IntertwiningMap (spechtRep t) ((spechtRep a).tprod (spechtRep b))). This is the standard polytabloid construction (and IsIrreducible of the chosen Specht module is part of the universal statement), but it is not Mathlib’s notion, so Saxl’s statement is only as faithful as this construction.
“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.
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.
The formalization proves the universal tensor-square conjecture for symmetric groups in the stated range. For every positive integer $n\notin\{2,4,9\}$, it constructs an irreducible complex representation of $S_n$ whose tensor square contains every irreducible complex representation of $S_n$. Equivalently, all corresponding Kronecker coefficients are positive. The statement also supplies injective intertwining maps for arbitrary finite-dimensional irreducible representations.
Saxl’s conjecture asserts that the tensor square of each staircase Specht module contains every irreducible representation of the corresponding symmetric group. The formalization establishes this for every $m\ge1$: if $\rho_m=(m,m-1,\ldots,1)$, then $g(\rho_m,\rho_m,\mu)>0$ for every partition $\mu$ of $m(m+1)/2$.
The stronger claim that every constituent appears in the orbit span of one prescribed tensor is not included.
AI-drafted comparisons, with no recorded human review
Saxl’s conjectureSaxl
Unreviewed AI draft: states a paper’s theorem as the paper does. States Saxl’s conjecture as stated in the cyclic-polytabloid paper: the tensor square of every staircase Specht module contains every irreducible representation. The stronger orbit-span claim is not included.
Universal irreducible tensor squares for symmetric groupsUniversalTensorSquares
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: for every n ∉ {2, 4, 9}, an irreducible representation of S_n whose tensor square contains every irreducible representation.
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.
Saxl’s conjectureSaxl
Three 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.
Universal irreducible tensor squares for symmetric groupsUniversalTensorSquares
One report, at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“REFUSED”
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Other people’s accounts of running proof-verification software, with links to their reports.
realopjt, realopjt/tensor-square-finite-check: independent check of the finite range (n up to 64) for symmetric-group tensor squares, 7 October 2026. Source
realopjt reports an independent check of the finite range, n at most 64.
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.
Proposition 7.1 of Universal Tensor Squares for Symmetric Groups, 24 September 2026
Reported by
cert-machine
Method
Exact computation
Their verdict
“CERTIFIED” Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: Proposition prop:finite-check for every eligible n <= 64 (61 of the 61 degrees), with witnesses supplied and certified here (the release records none: NEEDS DATA for its own certificate); the large-degree theory (n > 64) is not decided”
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.
Follow-up work by others
Keith Adler, keithadler/saxl-lean: independent Lean formalisation of the Saxl conjecture proof, 7 October 2026. Source
Independent Lean proofs of Saxl’s conjecture for staircases up to size 10 (S_1, S_3, S_6, S_10).
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 “Solid publication, could lead to tenure”. The page says that nothing on it is verified.
tparker, Philip Weiss, Will Sawin, Nik Weaver, Pace Nielsen, mathworker21, Joshua P. Swanson, Timothy Chow, Daniel Soltesz, MathOverflow: how many of the released results went against the conventional wisdom?, 10 October 2026. Source
The same expert notes that Saxl’s conjecture was proved true, in line with the universal expectation of those who had heard of it.
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
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
Run Comparator on OpenAI’s proof
Atlas records no independent report that Comparator accepted the proof at the release version shown here.Open the form
Identify the theorem the catalogue describes
Family 205The 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
The challenge statements imply the headline claim after unpacking definitions or one routine step.
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 the headline as OpenAI wrote it.
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 with Lean’s kernel: accepted (the check took 272 s; peak memory 6.5 GiB).
Date
11 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
Proposition 7.1 of Universal Tensor Squares for Symmetric Groups, 24 September 2026
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: Proposition prop:finite-check for every eligible n <= 64 (61 of the 61 degrees), with witnesses supplied and certified here (the release records none: NEEDS DATA for its own certificate); the large-degree theory (n > 64) is not decided”
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.