Constructs a three-dimensional complete Noetherian normal local domain over ℂ with no nonzero finitely generated maximal Cohen–Macaulay module. A three-dimensional local domain essentially of finite type over ℂ has the same property, disproving the domain form of the small Cohen–Macaulay module conjecture. (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 A Complete Local Domain without a Small Cohen–Macaulay Module, 23 September 2026
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.
There exists a three-dimensional complete Noetherian normal local domain R containing \C, with residue field \C, such that no nonzero finitely generated R-module has depth three.
In A Complete Local Domain without a Small Cohen–Macaulay Module, 23 September 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
Let X be a smooth integral projective surface over \C, and let H be an ample globally generated divisor. If R(X,H) admits a small Cohen–Macaulay module, then
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.
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. 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.
SurfaceConeCandidateSupportThe paper states
In A Complete Local Domain without a Small Cohen–Macaulay Module, 23 September 2026
There exists a three-dimensional complete Noetherian normal local domain R containing \C, with residue field \C, such that no nonzero finitely generated R-module has depth three.
The words they share: complete, residue, field, noetherian, domain, local, dimensional, three.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
SurfaceConeCandidateSupport.lean, the release lists it as a main result.
theorem candidate_ring_properties : ∃ (R : Type) (_ : CommRing R) (_ : IsDomain R) (_ : IsNoetherianRing R) (_ : IsIntegrallyClosed R) (_ : IsLocalRing R) (_ : Algebra ℂ R), IsAdicComplete (IsLocalRing.maximalIdeal R) R ∧ ringKrullDim R = 3 ∧ Function.Bijective (algebraMap ℂ (IsLocalRing.ResidueField R)) := 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
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 a supporting result (their term: “supporting-only”).
Their note: Lean states only that some C-algebra R is a three-dimensional, m-adically complete, Noetherian, integrally closed local domain with residue field C; it never mentions modules, depth or Cohen-Macaulayness, so the defining property of the headline (no nonzero finitely generated module of depth 3) and the essentially-finite-type corollary are not stated. As typed the existential is also satisfied by C[[x,y,z]] and does not name the surface cone, so it records only the ring-theoretic half of the construction.
Definitions the group asks readers to compare with the paper: candidate_ring_properties (the statement itself): a bare existence claim over an unconstrained R; it is not tied to the paper’s completed section ring R(X,H) (the proof uses ExplicitCone.completedRing, the statement does not mention it) and is satisfied by the regular ring C[[x,y,z]]; the key property (no nonzero finitely generated module of depth three) is absent.; IsIntegrallyClosed R: R is integrally closed in its fraction field (normal domain); standard.; IsAdicComplete (IsLocalRing.maximalIdeal R) R: R is Hausdorff and complete for the maximal-ideal-adic topology; standard.; ringKrullDim R = 3: Krull dimension 3 (value in WithBot N-infinity); standard.; Function.Bijective (algebraMap C (IsLocalRing.ResidueField R)): the structure map C -> R/m is bijective, i.e. residue field C; standard.; Algebra C R: the paper’s ‘containing C’ is encoded as an algebra structure over C; standard.
“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 supporting result (their term: “SUPPORT-ONLY”).
The gap they name: The counterexample itself (no nonzero finitely generated MCM module) and the essentially-of-finite-type example are not stated; only properties of the candidate ring are, and those properties are existential.
“SUPPORT-ONLY”, in their words: The challenge statements state only supporting results.
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 small Cohen–Macaulay module conjecture asks whether every complete local domain has a nonzero finitely generated maximal Cohen–Macaulay module. The linked formalization verifies only the ring-theoretic candidate: there exists a three-dimensional complete Noetherian integrally closed local domain over $\mathbb C$ whose residue field is $\mathbb C$.
It does not prove that this ring lacks a nonzero finitely generated maximal Cohen–Macaulay module, or the paper’s counterexample essentially of finite type.
Ring-theoretic properties of the completed surface-cone candidate SurfaceConeCandidateSupport
Unreviewed AI draft: states a supporting result. States only that the candidate ring is a three-dimensional complete Noetherian normal local domain over C with residue field C, one of the five supporting comparisons named in the Comparator README. The absence of a small Cohen–Macaulay module, the paper’s claim, is outside this statement.
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.
SurfaceConeCandidateSupportThree 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 |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 282 s; peak memory 6.4 GiB). | 10 October 2026 | Original report |
Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.
mo271, Wikipedia/SmallCohenMacaulayModules: exists_isSmallCohenMacaulay is false (issue 6912), 7 October 2026. Source
The release constructs a three-dimensional complete local domain with no nonzero finitely generated maximal Cohen-Macaulay module, refuting the statement.
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.
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 the Lean statement with the paperSuggest 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 counterexample and rates its significance, if it holds up, as “Career-defining publication”. 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 A Complete Local Domain without a Small Cohen–Macaulay Module, 23 September 2026
Why this passage is shown
Theorem 1.2
In A Complete Local Domain without a Small Cohen–Macaulay Module, 23 September 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, SurfaceConeCandidateSupport
Proof-verification report
MathVet, SurfaceConeCandidateSupport
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, SurfaceConeCandidateSupport
Lean statement
SurfaceConeCandidateSupport