∑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

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed 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 →