∑math20

Algebra · Result 195

A counterexample to the small Cohen–Macaulay module conjecture

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of A Complete Local Domain without a Small Cohen–Macaulay Module

A Complete Local Domain without a Small Cohen–Macaulay Module

OpenAI · September 23, 2026

We construct a three-dimensional complete Noetherian normal local domain containing ℂ, with residue field ℂ, that has no nonzero finitely generated maximal Cohen–Macaulay module. This disproves the domain form of the small Cohen–Macaulay module conjecture.

Read PDF Download Source

Cite
@misc{OAI:A-Complete-Local-Domain-Without-a-Small-Cohen-Macaulay-Module-September-23-2026,
  author = {{OpenAI}},
  title = {{A Complete Local Domain without a Small Cohen--Macaulay Module}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Complete-Local-Domain-Without-a-Small-Cohen-Macaulay-Module-September-23-2026/paper.pdf}{OAI:A-Complete-Local-Domain-Without-a-Small-Cohen-Macaulay-Module-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

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.

Comparator links

ResultComparator statement
Ring-theoretic properties of the completed surface-cone candidateSurfaceConeCandidateSupport.lean

Scope note on GitHub →