# A counterexample to the small Cohen–Macaulay module conjecture

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

- [A Complete Local Domain without a Small Cohen–Macaulay Module](../../preprints/A-Complete-Local-Domain-Without-a-Small-Cohen-Macaulay-Module-September-23-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Ring-theoretic properties of the completed surface-cone candidate | [SurfaceConeCandidateSupport.lean](../ComparatorChallenges/SurfaceConeCandidateSupport.lean) |