AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

A Complete Local Domain without a Small Cohen–Macaulay Module

Can the mathematical statement in A Complete Local Domain without a Small Cohen–Macaulay Module be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 195)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A Complete Local Domain without a Small Cohen–Macaulay Module'. 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.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 195). The Lean development was not rebuilt locally.