Lech's multiplicity conjecture - Revision history

Aftermath bot: Formalization: the Dutta comparison is the domain, characteristic-p case of Iyengar-Ma-Walker Conjecture 8.1, per the manuscript

2026-10-16T14:36:49Z

Formalization: the Dutta comparison is the domain, characteristic-p case of Iyengar-Ma-Walker Conjecture 8.1, per the manuscript

← Older revision		Revision as of 07:36, 16 October 2026
Line 21:		Line 21:
	** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/194.md 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 scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/194.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/DuttaDomain.lean DuttaDomain.lean] states <code>dutta_domain : DuttaDomainClaim</code> for complete Noetherian local domains of prime characteristic.		** The Comparator challenge [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/DuttaDomain.lean DuttaDomain.lean] states <code>dutta_domain : DuttaDomainClaim</code> for complete Noetherian local domains of prime characteristic.
			** The manuscript describes the corresponding corollary (''χ''<sub>∞</sub>(''F'') ≥ ''e''(''R'') for every short complex ''F'' over a complete Noetherian local domain of characteristic ''p'' > 0) as the case of complete local domains of positive characteristic in Conjecture 8.1 of Iyengar, Ma and Walker ([https://arxiv.org/abs/2104.10140v2 arXiv:2104.10140v2]; ''Algebra & Number Theory'' 16 (2022)). That conjecture asserts ''χ''<sub>∞</sub>(''F'') ≥ ''e''(''R'') for every short complex over any complete local ring. Their Proposition 8.3 shows that the full conjecture implies Lech's conjecture. The manuscript adds that the domain case is a consequence of its uniform estimate, not an assumption in its proof of Lech's conjecture.

	== Public follow-up work ==		== Public follow-up work ==

Aftermath bot: Follow-ups: cert-machine's public two-kernel run (Lean default kernel and nanoda accept the challenge)

2026-10-16T12:42:49Z

Follow-ups: cert-machine's public two-kernel run (Lean default kernel and nanoda accept the challenge)

← Older revision		Revision as of 05:42, 16 October 2026
Line 29:		Line 29:
	\|-		\|-
	\| 2026-10-10 to 2026-10-14 \|\| [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) \|\| Verification (second kernel) \|\| In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list <code>DuttaDomain</code>. The challenge was therefore accepted by con-leche and by Lean's official kernel. \|\| Development journal.		\| 2026-10-10 to 2026-10-14 \|\| [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) \|\| Verification (second kernel) \|\| In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list <code>DuttaDomain</code>. The challenge was therefore accepted by con-leche and by Lean's official kernel. \|\| Development journal.
			\|-
			\| 2026-10-10 \|\| [https://github.com/carlostoledo1891/cert-machine/blob/32739df1a7e9b09f6b56216444fa32927ffdeaad/corpus/openai-math/kernel-runs/38040214623/DuttaDomain.json cert-machine], openai/math lane K, run 38040214623 \|\| Verification (two kernels) \|\| Records that Lean's default kernel and the nanoda kernel accept the <code>DuttaDomain</code> solution (1,812 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. \|\| Repository.
	\|-		\|-
	\| 2026-10-12 \|\| [https://github.com/anantgupta2/AI-hard/tree/d6a2caf72ce9958eb87bf510b82b46a7080ca160/data/pilot/194 AI-hard], family 194 analysis (<code>family.md</code>, <code>novelty.md</code>, <code>downstream.md</code>; commit <code>d6a2caf</code>) \|\| 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 <code>DuttaDomain</code> comparator's dependency chain (<code>complex_estimate_basis</code>, for an abstract length with a weakened filtered-colimit axiom). It grades that estimate as its highest novelty level, with confidence 0.35. \|\| Repository.		\| 2026-10-12 \|\| [https://github.com/anantgupta2/AI-hard/tree/d6a2caf72ce9958eb87bf510b82b46a7080ca160/data/pilot/194 AI-hard], family 194 analysis (<code>family.md</code>, <code>novelty.md</code>, <code>downstream.md</code>; commit <code>d6a2caf</code>) \|\| 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 <code>DuttaDomain</code> comparator's dependency chain (<code>complex_estimate_basis</code>, for an abstract length with a weakened filtered-colimit axiom). It grades that estimate as its highest novelty level, with confidence 0.35. \|\| Repository.

Aftermath bot: New page from public sources: OpenAI's Lech manuscript (claim, method as described), scope note and comparator, MathVet, con-leche, AI-hard analysis

2026-10-16T12:04:35Z

New page from public sources: OpenAI's Lech manuscript (claim, method as described), scope note and comparator, MathVet, con-leche, AI-hard analysis

New page

'''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 ([https://github.com/openai/math 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''1, …, ''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''0''F'') ≥ λ(''C''/''I'')''s''''h''(rank ''F''0 − ''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, [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-Complete-Local-Domain-Without-a-Small-Cohen-Macaulay-Module-September-23-2026 ''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.''' [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Lechs-multiplicity-conjecture-September-23-2026 ''Lech's multiplicity conjecture''] in the openai/math repository (commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.'''
** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/194.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/DuttaDomain.lean DuttaDomain.lean] states <code>dutta_domain : DuttaDomainClaim</code> for complete Noetherian local domains of prime characteristic.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>DuttaDomain</code>. || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list <code>DuttaDomain</code>. The challenge was therefore accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-12 || [https://github.com/anantgupta2/AI-hard/tree/d6a2caf72ce9958eb87bf510b82b46a7080ca160/data/pilot/194 AI-hard], family 194 analysis (<code>family.md</code>, <code>novelty.md</code>, <code>downstream.md</code>; commit <code>d6a2caf</code>) || 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 <code>DuttaDomain</code> comparator's dependency chain (<code>complex_estimate_basis</code>, 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.

[[Category:OpenAI results]]