Algebra·OpenAI Math·Result 194·Lean formalisation listed
Lech’s multiplicity conjecture
One of the 372 results in OpenAI's public mathematics catalogue, filed under algebra: 1 preprint, the latest dated 23 September 2026. This page quotes OpenAI's own summary of the claim, links the paper and abstract, and will embed the animation.
Latest paper
Lech's multiplicity conjecture
The animation for this result has not been released yet. Subscribe on YouTube to catch it.
What OpenAI claims
Proves e(R) ≤ 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. (Lean)
Paper
Lech's multiplicity conjecture
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.
Status
Preprint. The paper has not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
Related results in Algebra
- 195A counterexample to the small Cohen–Macaulay module conjectureLean
- 196A counterexample to Kaplansky’s zero-divisor conjectureLean
- 197A torsion-free group algebra that is not directly finiteLean
- 198A counterexample to finitistic-dimension finitenessLean
- 199Counterexamples to Auslander–Reiten, Tachikawa and related homological conjecturesLean
- 200Eisenbud–Green–Harris and lex-plus-powers
