Lech's multiplicity conjecture

Follow-up works

• S. B. Iyengar, L. Ma, M. Walker, Lech's conjecture in equal characteristic (preliminary draft, 20 pp., posted on Walker's website, October 2026). A human-written account of a separate AI-generated proof of the equal-characteristic case (found by Alex Gerko with ChatGPT Astra), going through a Dutta-multiplicity lower bound $\chi_\infty(F)\ge e(R)$ in characteristic $p$ and a length bound for "deep" finite free resolutions inspired by Boij–Söderberg theory. This parallels this paper's uniform complex estimate and its Dutta corollary. [AI-generated per source]

Comments and discussion

• Mark Walker (with S. B. Iyengar and L. Ma), Lech's conjecture in equal characteristic (project page) (personal website, posted 5 October 2026, updated 6 October 2026). The page hosts the exposition, the original AI-written manuscript and two AI-prepared provenance notes, and links this paper, noting that it covers the general case, not only equal characteristic.
• mahrud on GitHub, 194. Lech's multiplicity conjecture (PR #194, mahrud/openai-math-comments) (9 October 2026). An inline comment on the introduction says the core idea of the uniform estimate "seems to be a generalization of the core idea in the proof at https://mark-walker-22.github.io/Lech.html". Another comment notes that the Lean proof does not cover the full preprint.

Formalization

• OpenAI math release, Lean scope note lean/docs/194.md (OpenAI Math Release, 2026-10-06). The formalization covers convergence of the Frobenius multiplicity sequence and the comparison $e(D)\le\chi_\infty(F)$ for short complexes over complete local domains of characteristic $p$. It does not cover the flat-local main theorem in arbitrary characteristic.
• OpenAI math release, DuttaDomain.lean (theorem dutta_domain) (openai/math, 2026). The Lean proof file for the complete-domain Dutta comparison (statement in lean/ComparatorChallenges/DuttaDomain.lean), a 54-line file delegating to the auxiliary lemma dutta_complete_charp and importing OAI.RingTheory.Multiplicity.DuttaAlgClosed.

Related prior literature mentioned by others

• D. Eisenbud, G. Fløystad, F.-O. Schreyer, Sheaf cohomology and free resolutions over exterior algebras (arXiv:math/0104203; Trans. AMS 355 (2003)). Iyengar–Ma–Walker's equal-characteristic exposition cites this paper for its graded positivity lemma, the analogue of this paper's Eisenbud–Schreyer vector-bundle step. It is not in this paper's bibliography.
• C. Peskine, L. Szpiro, Dimension projective finie et cohomologie locale (Publ. Math. IHÉS 42 (1973), 47–119). The Iyengar–Ma–Walker exposition cites this source for the Frobenius functor and the acyclicity lemma used in defining and bounding the Dutta multiplicity. It is not in this paper's bibliography.

Possibly relevant literature (found by the agent, not checked)

• Craig Huneke, Linquan Ma, Pham Hung Quy and Ilya Smirnov, Asymptotic Lech's inequality (arXiv:1907.08344, 2019-07-19; revised 2020-07-16). Its uniform approximation of Hilbert–Kunz multiplicity by colength (completion reduced, equidimensional, isolated singularity) is related background for the manuscript's characteristic-$p$ length estimates used in the multiplicity comparison.