Theorem 1.1
In An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
A stable-coordinate counterexample in four variables
Constructs a polynomial in four complex variables that is not a coordinate but becomes one after adjoining a single variable, disproving the Stable Coordinate conjecture in four variables. Every fiber is affine three-space, yet none of its embeddings is rectifiable, also disproving the Abhyankar–Sathaye conjecture even when all fibers are affine spaces. (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
What the papers state
Corollary 1.2
In An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
For every integer n\ge4, there is a polynomial f\in\CC[z_1,\ldots,z_n] such that \CC[z_1,\ldots,z_n]/(f)\cong\CC^{[n-1]} and f is not a coordinate.
Corollary 1.2
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
For every \lambda\in\C, the hypersurface f^{-1}(\lambda)\subset\A^4 is isomorphic to \A^3 and its embedding in \A^4 is not rectifiable.
No Lean statement in the release is paired with this theorem.
The release does not say which paper theorem its catalogue describes. The statements above share the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.
One more possible match
- Theorem 1.1 in A stable coordinate that is not a coordinate in four variables, 5 October 2026.
- Reported proof verification
- Three Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
- Papers and explanations
- Two current papers, each readable here as a page beside its PDF.
Papers
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.
A stable coordinate that is not a coordinate in four variables
We construct an explicit degree-five polynomial over \(\mathbf C\) that is not a coordinate in four variables but becomes one after adjoining a single variable. This gives a counterexample to the stable coordinate conjecture in four variables. Every fiber is isomorphic to affine three-space, yet its embedding in affine four-space is not rectifiable. Thus the example also disproves the Abhyankar–Sathaye embedding conjecture in ambient dimension four.
An explicit noncoordinate polynomial with affine three-space zero fibre
We construct an explicit counterexample to the Abhyankar–Sathaye conjecture: a noncoordinate polynomial in four complex variables whose zero fibre is affine three-space. Adjoining variables gives counterexamples in every ambient dimension at least four.
Three 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.
AbhyankarSathaye
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:
- Theorem 1.1 in An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026.
- Corollary 1.2 in An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026.
- Proposition 2.3 in A stable coordinate that is not a coordinate in four variables, 5 October 2026.
- Proposition 2.2 in A stable coordinate that is not a coordinate in four variables, 5 October 2026.
- Theorem 1.1 in A stable coordinate that is not a coordinate in four variables, 5 October 2026.
- Proposition 2.1 in A stable coordinate that is not a coordinate in four variables, 5 October 2026.
- Proposition 3.3 in A stable coordinate that is not a coordinate in four variables, 5 October 2026.
- Proposition 3.1 in A stable coordinate that is not a coordinate in four variables, 5 October 2026.
The Lean statement
No paper theorem is paired with it.
Noncoordinate polynomial in every dimension at least four
AbhyankarSathaye.lean, the release lists it as a main result.
theorem exists_noncoordinate_polynomial (n : ℕ) (hn : 4 ≤ n) : ∃ F : MvPolynomial (Fin n) ℂ, Nonempty ((MvPolynomial (Fin n) ℂ ⧸ Ideal.span {F}) ≃ₐ[ℂ] MvPolynomial (Fin (n - 1)) ℂ) ∧ ¬ ∃ (equiv : MvPolynomial (Fin n) ℂ ≃ₐ[ℂ] MvPolynomial (Fin n) ℂ) (index : Fin n), equiv (MvPolynomial.X index) = F := 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.
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”.
CommutingDerivations
The paper states
Corollary 1.2
In An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026
For every integer n\ge4, there is a polynomial f\in\CC[z_1,\ldots,z_n] such that \CC[z_1,\ldots,z_n]/(f)\cong\CC^{[n-1]} and f is not a coordinate.
The words they share: integer, polynomial, coordinate.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
Commuting locally nilpotent derivations
CommutingDerivations.lean, the release lists it as a main result.
theorem commuting_derivations_with_ordinary_extras (n : ℕ) (hn : 4 ≤ n) : ∃ d : Fin (n-1) → Derivation ℂ (MvPolynomial (Fin n) ℂ) (MvPolynomial (Fin n) ℂ), (∀ i, d i (extendedF hn + 1) = 0) ∧ (∀ i j p, d i (d j p) = d j (d i p)) ∧ (∀ i, LocallyNilpotent (d i)) ∧ LinearIndependent (MvPolynomial (Fin n) ℂ) d ∧ (∀ p, (∀ i, d i p = 0) ↔ p ∈ Algebra.adjoin ℂ ({extendedF hn} : Set (MvPolynomial (Fin n) ℂ))) ∧ (∀ g, (∀ i, d i g = 0) → ¬ ∃ (e : MvPolynomial (Fin n) ℂ ≃ₐ[ℂ] MvPolynomial (Fin n) ℂ) (j : Fin n), e (X j) = g) ∧ (∀ i : Fin (n-4), d (blocksToOutput hn (Sum.inl i)) = pderiv (blocksToAmbient hn (Sum.inl i))) := 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.
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”.
StableCoordinateFour
The paper states
Theorem 1.1
In An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026
The words they share: polynomial, coordinate, noncoordinate, affine, space, explicit, three.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
Degree-five stable noncoordinate with nonrectifiable affine-space fibers
StableCoordinateFour.lean, the release lists it as a main result.
def PrincipalPackage : Prop := PolynomialPackage ∧ FiberPackagetheorem principal_package : PrincipalPackage := 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
- cert-machine records it as “CERTIFIED”.
- MathVet records it as “comparator-sandboxed-pass”.
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: StableCoordinateFour.principal_package unfolds (PrincipalPackage = PolynomialPackage ∧ FiberPackage) to: the explicit f (same Q and f as the paper’s Theorem thm:main) has totalDegree 5, is a coordinate of ℂ[x0..x4] after rename Fin.castSucc, and is not a coordinate of ℂ[x0..x3]; moreover every fibre f = t has coordinate ring ≅ ℂ[y1,y2,y3] and no automorphism carries (f − t) onto (x0). The only steps are definition unfolding (and f − C 0 = f for the Abhyankar–Sathaye reading at t = 0), so both the stable-coordinate claim and the fibre/Abhyankar–Sathaye claim are stated; AbhyankarSathaye (all n ≥ 4) and CommutingDerivations go beyond the headline.
Definitions the group asks readers to compare with the paper: IsCoordinate: ∃ ℂ-algebra automorphism φ of R n with φ g = X 0; equivalent to g being the image of a variable (or a member of a polynomial generating set), standard; IsOneStableCoordinate: φ (stabilize g) = X 0 for an automorphism φ of R 5, with stabilize = rename Fin.castSucc; standard (adjoin one variable); IsAffineThreeSpaceFiber / FiberRing: the scheme-theoretic fibre ring R 4 ⧸ span {f − C t} is ℂ-algebra isomorphic to R 3; standard; IsRectifiableFiber: some ℂ-automorphism φ of R 4 maps the ideal (f − C t) onto (X 0); standard rectifiability, equivalent to f − t being a coordinate up to a nonzero scalar (the paper’s cor:fibers proof); StableCoordinateFour.PolynomialPackage includes f.totalDegree = 5 as an extra conjunct, matching the paper’s ‘explicit degree-five polynomial’; CommutingDerivations.fourInclusion / extendedF / blocksToAmbient / blocksToOutput: index bookkeeping; unfolding Equiv.sumComm, finSumFinEquiv (castAdd / natAdd) and finCongr (value-preserving Fin.cast) shows that for i < n−4 derivation number 3+i must equal ∂/∂x_(4+i) (the ordinary extra partials); derivations 0, 1, 2 are constrained only by the other conjuncts (they are not required to ignore the added variables); CommutingDerivations.LocallyNilpotent: ∀ a, ∃ n, D^[n] a = 0; standard; CommutingDerivations: LinearIndependent (MvPolynomial (Fin n) ℂ) d uses Mathlib’s R-module structure on Derivation ℂ R R (Derivation.instModule), i.e. independence over the polynomial ring; standard; CommutingDerivations S, P, h, u, v, w, x, y, s, p, F: the explicit F = h − P(x,y,s) − 1 of the September paper (matches eq:xyz and eq:F symbol by symbol); it is a different polynomial from StableCoordinateFour’s degree-five f; AbhyankarSathaye: no custom definitions; F is existentially quantified, not pinned to the explicit polynomial
“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.
cert-machine finds that the Lean statements express or imply the whole advertised result (their term: “MATCHES”).
“MATCHES”, in their words: 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.
OpenAI’s own note on what its Lean covers
The stable coordinate conjecture predicts that a polynomial that becomes a coordinate after adjoining variables was already a coordinate. The formalization gives an explicit degree-five polynomial in four complex variables that becomes a coordinate after adjoining one variable but is not a coordinate in four variables. Every fiber is isomorphic to affine three-space, yet no fiber can be carried to a coordinate hyperplane by an ambient polynomial automorphism.
The Abhyankar–Sathaye conjecture predicts that a polynomial defining an affine-space quotient must be an ambient coordinate. For every $n\ge4$, the formalized counterexample gives $F\in\mathbb C[x_1,\ldots,x_n]$ with quotient $\mathbb C[x_1,\ldots,x_n]/(F)\cong\mathbb C[y_1,\ldots,y_{n-1}]$, although $F$ is not a coordinate. A companion gives $n-1$ commuting, locally nilpotent derivations, linearly independent over the polynomial ring, whose common kernel is generated by the construction’s explicit polynomial and contains no ambient coordinate. The extra $n-4$ derivations are ordinary partial derivatives in the added variables. The three-variable case is not covered.
AI-drafted comparisons, with no recorded human review
Noncoordinate polynomial in every dimension at least four
AbhyankarSathayeUnreviewed AI draft: states a consequence of a paper’s theorem. States the paper’s corollary for every n ≥ 4 in existential form: some polynomial in n variables has quotient isomorphic to a polynomial ring in n − 1 variables without being a coordinate. The main theorem’s explicit four-variable polynomial is not named in the statement.
Commuting locally nilpotent derivations
CommutingDerivationsUnreviewed AI draft: states a consequence of a paper’s theorem. States a companion application of the paper’s explicit polynomial: n − 1 commuting, locally nilpotent, linearly independent derivations whose common kernel is generated by it and contains no coordinate. This is not one of the paper’s displayed theorem statements.
Degree-five stable noncoordinate with nonrectifiable affine-space fibers
StableCoordinateFourUnreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the four-variable paper (the explicit degree-five polynomial is a coordinate after adjoining one variable but not before) together with its corollary on nonrectifiable fibres.
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.
Noncoordinate polynomial in every dimension at least four AbhyankarSathaye
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. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 30 s; peak memory 2.1 GiB). | 10 October 2026 | Original report |
Commuting locally nilpotent derivations CommutingDerivations
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. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 35 s; peak memory 2.2 GiB). | 11 October 2026 | Original report |
Degree-five stable noncoordinate with nonrectifiable affine-space fibers StableCoordinateFour
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. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 10 October 2026 | Original report |
Other proofs and exact calculations
These reports examine claims in the papers using HOL Light, a different proof assistant and exact calculations for finite claims, independently of the release’s Lean proofs. Read each report for the exact claim it covers.
Two explicit polynomial maps on ℝ⁵ are mutually inverse and send the paper’s f to the first coordinate
HOL Light card 049
- Reported by
- Ben Knill, openai-math-hol-cards
- Method
- Proof of a selected step in HOL Light
- Their verdict
- “PASS” The report records a proof of a supporting fact.
- What it covers
- Independent polynomial-identity check; upstream fd4aeeb2 now also covers the October 5 stable-coordinate result. This HOL card does not prove its noncoordinate obstruction
- Original report
- Their report
A stable coordinate that is not a coordinate in four variables, 5 October 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: f is a one-stable coordinate (an explicit automorphism of C[x1..x4,w] with exhibited inverse sends f to x1), deg f = 5, and every fibre f = lambda is C^[3]; NOT that f is not a coordinate in four variables, which carries the counterexample”
- Original report
- Their report
An explicit noncoordinate polynomial with affine three-space zero fibre, 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
- “the whole headline: R/(F) = C^[3] by the paper’s printed mutually inverse maps, and grad F vanishes at a point, so F is not a coordinate”
- Original report
- Their report
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
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.
Offer to write an explanationCompare one Lean statement with its paper: AbhyankarSathaye, CommutingDerivations, StableCoordinateFourSuggest a source attributionSuggest a change
What people have said
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 counterexample and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.
Author not stated. Source
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The headline claims a stable-coordinate counterexample, but the formalised polynomial has a critical point, so it is not a stable coordinate.
From github.com/VolMax-Studio/p10-openai-math-verification-pilot, 7 October 2026. Source
At the 6 October commit the family headline (a stable-coordinate counterexample) was not what AbhyankarSathaye states, and the scope note did not link the 5 October manuscript. Both were resolved at fd4aeeb2, which links that manuscript and adds StableCoordinateFour.
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
- 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 049 No single paper statement clearly matches OpenAI’s description by wording, and no review identifying the intended theorem is recorded. Open the form
Address a question raised in an independent assessment
- Family 049 MathVet: its request is printed in full under the outside readers. Open the form
Compare the proposed paper and Lean matches
- Family 049 Atlas 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
In An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026
- How it was found
- Its words were compared with the words of OpenAI’s catalogue description.
- Words they share
- coordinate, polynomial
- Review
- Atlas records no review confirming that this is the theorem OpenAI’s description refers to.
- The record’s reason
- No unique candidate with at least three shared catalogue terms.
Why this passage is shown
Corollary 1.2
In An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026
- How it was found
- Its words were compared with the words of OpenAI’s catalogue description.
- Words they share
- coordinate, polynomial
- Review
- Atlas records no review confirming that this is the theorem OpenAI’s description refers to.
- The record’s reason
- No unique candidate with at least three shared catalogue terms.
Why this passage is shown
Corollary 1.2
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
- How it was found
- Its words were compared with the words of OpenAI’s catalogue description.
- Words they share
- fibers, rectifiable
- Review
- Atlas records no review confirming that this is the theorem OpenAI’s description refers to.
- The record’s reason
- No unique candidate with at least three shared catalogue terms.
Why this passage is shown
Theorem 1.1
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
- How it was found
- Its words were compared with the words of OpenAI’s catalogue description.
- Review
- Atlas records no review confirming that this is the theorem OpenAI’s description refers to.
- The record’s reason
- No unique candidate with at least three shared catalogue terms.
Why this passage is shown
Theorem 1.1
In An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026
- How it was found
- Its words were compared with the words of the Lean statement AbhyankarSathaye.
- Words they share
- polynomial, coordinate, noncoordinate, affine, space, cong
- Review
- Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Corollary 1.2
In An explicit noncoordinate polynomial with affine three-space zero fibre, 24 September 2026
- How it was found
- Its words were compared with the words of the Lean statement AbhyankarSathaye.
- Words they share
- integer, polynomial, coordinate, cong
- Review
- Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition 2.3
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
- How it was found
- Its words were compared with the words of the Lean statement AbhyankarSathaye.
- Words they share
- ring, polynomial, quotient
- Review
- Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition 2.2
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
- How it was found
- Its words were compared with the words of the Lean statement AbhyankarSathaye.
- Words they share
- ring, polynomial, coordinates
- Review
- Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Theorem 1.1
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
- How it was found
- Its words were compared with the words of the Lean statement AbhyankarSathaye.
- Words they share
- four, coordinate
- Review
- Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition 2.1
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
- How it was found
- Its words were compared with the words of the Lean statement AbhyankarSathaye.
- Words they share
- polynomial, coordinates
- Review
- Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition 3.3
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
- How it was found
- Its words were compared with the words of the Lean statement AbhyankarSathaye.
- Words they share
- ring, coordinate
- Review
- Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition 3.1
In A stable coordinate that is not a coordinate in four variables, 5 October 2026
- How it was found
- Its words were compared with the words of the Lean statement AbhyankarSathaye.
- Words they share
- ring
- Review
- Atlas records no review confirming that the two statements mean the same thing.
Independent assessment
MathVet
- Their term
- “full”
- What their term means
- 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.
- Version
14c7f91- Licence
- Apache-2.0
Independent assessment
Carlos Toledo’s cert-machine
- Their term
- “MATCHES”
- What their term means
- 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…
- Version
9814e4c- Licence
- MIT
Proof-verification report
cert-machine, AbhyankarSathaye
- Their word
- “CERTIFIED”
- Their account
- Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
- 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.
Proof-verification report
MathVet, AbhyankarSathaye
- Their word
- “comparator-sandboxed-pass”
- Their account
- 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.
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, AbhyankarSathaye
- Their word
- “accepted”
- Their account
- Re-run through Comparator with Lean’s kernel: accepted (the check took 30 s; peak memory 2.1 GiB).
- Date
- 10 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.
Proof-verification report
cert-machine, CommutingDerivations
- Their word
- “CERTIFIED”
- Their account
- Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
- 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.
Proof-verification report
MathVet, CommutingDerivations
- Their word
- “comparator-sandboxed-pass”
- Their account
- 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.
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, CommutingDerivations
- Their word
- “accepted”
- Their account
- Re-run through Comparator with Lean’s kernel: accepted (the check took 35 s; peak memory 2.2 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.
Proof-verification report
cert-machine, StableCoordinateFour
- Their word
- “CERTIFIED”
- Their account
- Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
- 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.
Proof-verification report
MathVet, StableCoordinateFour
- Their word
- “comparator-sandboxed-pass”
- Their account
- Re-run through Comparator in a sandboxed virtual machine: accepted.
- Date
- 10 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.
Report using another proof or calculation method
Two explicit polynomial maps on ℝ⁵ are mutually inverse and send the paper’s f to the first coordinate
Proofs of selected steps in HOL Light, Ben Knill, openai-math-hol-cards
- Their verdict
- “PASS”
- Claim tested or proved
- Two explicit polynomial maps on ℝ⁵ are mutually inverse and send the paper’s f to the first coordinate
- What it covers
- Independent polynomial-identity check; upstream fd4aeeb2 now also covers the October 5 stable-coordinate result. This HOL card does not prove its noncoordinate obstruction
- Version
68a1228
Report using another proof or calculation method
A stable coordinate that is not a coordinate in four variables, 5 October 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: f is a one-stable coordinate (an explicit automorphism of C[x1..x4,w] with exhibited inverse sends f to x1), deg f = 5, and every fibre f = lambda is C^[3]; NOT that f is not a coordinate in four variables, which carries the counterexample”
- Version
9814e4c
Report using another proof or calculation method
An explicit noncoordinate polynomial with affine three-space zero fibre, 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
- “the whole headline: R/(F) = C^[3] by the paper’s printed mutually inverse maps, and grad F vanishes at a point, so F is not a coordinate”
- Version
9814e4c
Lean statement
AbhyankarSathaye
- Statement
- Noncoordinate polynomial in every dimension at least four
- Role
- the release lists it as a main result
- Paired with
- No paper theorem is paired with this Lean statement.
- Who ran the proof-verification program
- three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Lean statement
CommutingDerivations
- Statement
- Commuting locally nilpotent derivations
- Role
- the release lists it as a main result
- Paired with
- Corollary 1.2 (candidate pairing)
- Who ran the proof-verification program
- three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Lean statement
StableCoordinateFour
- Statement
- Degree-five stable noncoordinate with nonrectifiable affine-space fibers
- Role
- the release lists it as a main result
- Paired with
- Theorem 1.1 (candidate pairing)
- Who ran the proof-verification program
- two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet.