∑math20

Algebra · Result 194

Lech’s multiplicity conjecture

1 paperLean

Proves \(e(R)\le e(S)\) for every flat local homomorphism of nonzero Noetherian local rings, where e is Hilbert–Samuel multiplicity. This resolves Lech's conjecture in every dimension and characteristic.

Watch

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

Papers 1

First page of Lech's multiplicity conjecture

Lech's multiplicity conjecture

OpenAI · September 23, 2026

We prove Lech's multiplicity conjecture: Hilbert–Samuel multiplicity cannot decrease under a flat local homomorphism of nonzero Noetherian local rings. The result holds in arbitrary dimension, with no restrictions on the residue fields or characteristics.

Read PDF Download Source

Cite
@misc{OAI:Lechs-multiplicity-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{Lech's multiplicity conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Lechs-multiplicity-conjecture-September-23-2026/paper.pdf}{OAI:Lechs-multiplicity-conjecture-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

Lech's multiplicity conjecture compares Hilbert–Samuel multiplicities across flat local maps. The linked formalization covers a supporting characteristic-\(p\) comparison over a complete Noetherian local domain \(D\): for a complex satisfying the stated short-complex and finite-length homology conditions, its Frobenius multiplicity sequence converges to its Dutta multiplicity, and the Hilbert–Samuel multiplicity of \(D\) is at most that Dutta multiplicity.

This selected statement is the complete-domain Dutta comparison. The paper's full flat-local result in arbitrary characteristic is outside it.

Comparator links

ResultComparator statement
Complete-domain Dutta multiplicity comparisonDuttaDomain.lean

Scope note on GitHub →