Lech's multiplicity conjecture

Lech's multiplicity conjecture asserts that the Hilbert–Samuel multiplicity cannot decrease under a flat local homomorphism of Noetherian local rings: if (R, 𝔪) → (S, 𝔫) is flat and local, then e(R) ≤ e(S). A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a proof in arbitrary dimension, with no restriction on residue fields or characteristics. This page summarizes the published claim and lists publicly available follow-up work.

Background

• As recounted in the manuscript's introduction:
  • Lech (1960, 1964) proved the inequality when the source has dimension at most two, and in important cases with complete-intersection closed fiber.
  • Ma proved it for equal-characteristic sources of dimension three, and the bound e(R) ≤ max{1, d!/2^d} e(S) in equal characteristic.
  • Ma also proved it for standard graded sources over a perfect field, via weakly lim Ulrich sequences. Meng proved a complementary graded case.
• Hanes developed the Ulrich-module approach. Yhee constructed complete two-dimensional local domains admitting no weakly lim Ulrich sequence.
• Iyengar, Ma and Walker developed multiplicity inequalities for short free complexes. The manuscript describes their approach to Lech's conjecture as the predecessor of its construction.

The original result

• Claim. Theorem 1.1: for every flat local homomorphism (R, 𝔪) → (S, 𝔫) of nonzero Noetherian local rings, e(R) ≤ e(S). There is no restriction on dimensions, residue fields or characteristics.
• Method, as described in the manuscript. The main ingredient is a uniform estimate for finite free complexes (Theorem 2.1).
  • Setting: an ideal I = (z₁, …, z_h) in a possibly non-Noetherian ring, and an additive length λ satisfying stated stability hypotheses, under which the powers of z behave as a parameter system.
  • Estimate: a finite free complex F of length at most h, alternating rank zero, contractible off V(I), with differential entries in I^s, satisfies λ(H₀F) ≥ λ(C/I)s^h(rank F₀ − A_h Σ rank F_i/s) for large s. The constant does not depend on the ring or the length theory.
  • Proof of the estimate: a blowup comparison, together with the characteristic-free vector-bundle construction of Eisenbud and Schreyer. The bundle's cohomological roots are chosen near s times the roots of the derivative of ∏(x+i).
  • Application: the estimate is applied with perfection in characteristic p, and with the perfectoid normalized lengths of Cai, Lee, Ma, Schwede and Tucker in mixed characteristic. The manuscript also derives a Dutta-multiplicity consequence in characteristic p.
• Related manuscript in the collection. The introduction cites a companion, A Complete Local Domain without a Small Cohen–Macaulay Module. It constructs a complete three-dimensional normal local C-domain with no nonzero finitely generated maximal Cohen–Macaulay module. The manuscript uses it to argue that approaches needing such a module over every source cannot be universal.
• Source. Lech's multiplicity conjecture in the openai/math repository (commit 1581d4c).
• Formalization, as described by the repository.
  • The scope note lean/docs/194.md states that the formalization covers a supporting characteristic-p comparison over a complete Noetherian local domain. For a short complex with finite-length homology, its Frobenius multiplicity sequence converges to its Dutta multiplicity, and the Hilbert–Samuel multiplicity of the domain is at most that Dutta multiplicity. "The paper's full flat-local result in arbitrary characteristic is outside it."
  • The Comparator challenge DuttaDomain.lean states dutta_domain : DuttaDomainClaim for complete Noetherian local domains of prime characteristic.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 16 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "supporting-only": the challenge states the characteristic-p Dutta comparison over complete local domains, and the headline inequality e(R) ≤ e(S) is not stated. Records a sandboxed Comparator pass for DuttaDomain.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list DuttaDomain. The challenge was therefore accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-10	cert-machine, openai/math lane K, run 38040214623	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the DuttaDomain solution (1,812 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-12	AI-hard, family 194 analysis (family.md, novelty.md, downstream.md; commit d6a2caf)	Reading (novelty analysis)	A model-assisted, text-level analysis. Its literature checks are at search-snippet level, and the repository describes its analyses as "model-assisted judgements on unreviewed mathematics, not results". It reports that the headline is not formalized, but that the uniform complex estimate (Theorem 2.1) appears in the Lean files on the DuttaDomain comparator's dependency chain (complex_estimate_basis, for an abstract length with a weakened filtered-colimit axiom). It grades that estimate as its highest novelty level, with confidence 0.35.	Repository.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.