AI Proved What?

Episode 194, October 2026

Never smoother?

A preprint claims that Hilbert–Samuel multiplicity never drops along a flat map of local rings, in any dimension and any characteristic

Covers result 194 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

6:09. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:47The claim
  3. 2:59How the proof goes
  4. 5:15Where it stands

The claim, in plain words

Zoom in on a point and count how many independent functions survive up to each order. At a smooth point of a curve the count grows 1, 2, 3, …; at a cusp or where two lines cross it grows 1, 3, 5, 7, …, twice as fast. That growth rate, suitably scaled, is the Hilbert–Samuel multiplicity e: in our computations 1 at a smooth point, 2 for a cusp or a node, 3 for three lines through a point, 2 at the tip of a quadric cone. A flat map from a local ring R to another, S, is the algebraic version of a well-behaved family over R. Lech asked whether always e(R) ≤ e(S).

Flatness matters: unfolding a cusp onto a line drops e from 2 to 1, but that map is not flat. And flatness easily gives only an upper bound for e(S), e(R) times the length of the fibre when the fibre is a fat point. As the paper tells it, Lech proved the inequality for sources of dimension at most 2 and in cases with complete-intersection fibres; Ma proved it for equal-characteristic sources of dimension 3 and, in equal characteristic, in every dimension up to the constant max{1, d!/2d} (1.5 in dimension 4); Ma also proved standard graded sources, and Meng a graded case on the target side. Approaches through Ulrich modules met obstructions, one from a companion paper in the same release (result 195).

Result 194 is one OpenAI preprint, Lech’s multiplicity conjecture (41 pages, dated September 23, 2026). Its Theorem 1.1: for every flat local homomorphism (R, 𝔪) → (S, 𝔫) of nonzero Noetherian local rings, e(R) ≤ e(S), with no restriction on the dimensions, the residue fields or the characteristics. Along the way (Corollary 5.4) it proves the case of complete local domains of characteristic p of a conjecture of Iyengar, Ma and Walker: the Dutta multiplicity of a short complex is at least e(R).

What it doesn’t claim

A stronger inequality, a criterion for equality, or anything for maps that are not flat. The Iyengar–Ma–Walker conjecture beyond complete domains of characteristic p. The proof does not use Ulrich modules; result 195 is cited only to show that approaches needing a finitely generated Cohen–Macaulay module over every ring cannot work everywhere. Our examples are small rings over the rational numbers and only illustrate the definitions.

Where it stands

Posted as a preprint
OpenAI, 41 pages, dated September 23, 2026
Peer reviewed
Not yet
Checked in Lean
Not the main theorem: OpenAI’s Lean checks a supporting characteristic-p result; not run by us

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization, but its comparator statement is the supporting characteristic-p result (Corollary 5.4, about Dutta multiplicity), not Lech’s inequality; the files also contain the paper’s uniform estimate (Theorem 2.1) as an internal lemma. By our count they take 278 files and about 54,000 lines, excluding Mathlib (source). We found no unproved steps by search; we have not rebuilt the proof. The collection’s formalization.yaml does not list this result. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. Tidy up and factor. Complete, reduce to a zero-dimensional fibre, split R into irreducible pieces and enlarge the residue field (Lemma 4.2). Factor R → T → S = T/J with T “R plus smooth directions”, so e(T) = e(R), and combine a short free resolution of S over T with a Koszul complex on parameters: a short chain of matrices whose cokernel encodes e(S) (Proposition 4.3).
  2. The uniform estimate. If every matrix entry of such a chain lies in the s-th power of a parameter ideal, the cokernel is at least about sh times a fixed unit, with relative error O(1/s), uniformly in the ring and the length used (Theorem 2.1). The proof blows up the point and twists by an Eisenbud–Schreyer vector bundle whose roots sit near s times those of H′, H(x) = (x+1)(x+2)⋯(x+h), so that the layer sums in every degree share the leading term (h−1)! sh.
  3. Characteristic p. Frobenius makes entries deep; on the perfection the cokernel’s size is a Hilbert–Kunz multiplicity: e(S) = eHK(H,T) (Ma’s identity) ≥ e(T) = e(R) (Theorem 5.2).
  4. Mixed characteristic. Roots of parameters, Heitmann’s Briançon–Skoda theorem and perfectoid lengths, with two limits in a careful order (Theorem 6.3).
  5. Characteristic zero. A counterexample would be finitely many polynomial equations; Artin approximation and reduction modulo a prime would give one in characteristic p (§7).

The numbers in the video

  • Multiplicities (ours, over ℚ): smooth 1; cusp, node 2 (counts 1, 3, 5, 7, …); three lines 3; quadric cone 2.
  • Seven flat maps between small rings (ours): all satisfy e(R) ≤ e(S) ≤ e(R)·length(S/𝔪S); the cusp’s normalization (not flat) drops e from 2 to 1.
  • Ma’s constant max{1, d!/2d} for d = 1 to 6: 1, 1, 1, 1.5, 3.75, 11.25 (our arithmetic).
  • A plane case of the uniform estimate (ours): two plane curves each vanishing to order s meet at least s² times (classical), illustrated for s = 1 to 6. The roots of H′ for h = 4 and the layer sums are our numerics. The Lean count is our count of the import closure.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The question

Zoom in on a point of a curve or a surface, and count the polynomial wiggles that live there: how many independent functions survive up to each order. At a smooth point of a curve, the count goes 1, 2, 3, and so on. At a cusp, or where two lines cross, it goes 1, 3, 5, 7: twice as fast. That growth rate, suitably scaled, is the Hilbert–Samuel multiplicity, e: 1 at a smooth point, 2 for a cusp or a node, 3 for three lines through a point, 2 at the tip of a round cone, in our computations. A flat map from one local ring, R, to another, S, is the algebraic version of a well-behaved family sitting over R, with no fibres jumping in size. Lech asked: can such a map make the singularity better? Is e(R) always at most e(S)? Flatness matters: unfolding a cusp onto a line drops e from 2 to 1, but that map is not flat. And the easy comparison goes the wrong way: flatness readily gives an upper bound for e(S), the multiplicity of R times the length of the fibre when the fibre is a fat point, not the lower bound Lech asked for. As the paper tells it, Lech proved the inequality when the source has dimension at most 2, and in cases with complete-intersection fibres. Ma proved it for equal-characteristic sources of dimension 3, and, in equal characteristic, every dimension up to a constant: e(R) is at most max{1, d!/2^d}, times e(S). That constant is 1.5 in dimension 4, and grows fast after. Ma also proved it for standard graded sources, and Meng a graded case on the target side. Approaches through Ulrich modules met obstructions, one of them a companion paper in this same release.

1:47The claim

Result 194 is one OpenAI preprint, 41 pages, dated September 23, 2026. It claims: for every flat local homomorphism of nonzero Noetherian local rings, e(R) is at most e(S), with no restriction on the dimensions, the residue fields, or the characteristics. Along the way, it proves a case of a conjecture of Iyengar, Ma and Walker: over a complete local domain of characteristic p, the Dutta multiplicity of any short complex is at least the multiplicity of the ring. Not claimed: any stronger inequality, any criterion for equality, or anything for maps that are not flat; and the Iyengar, Ma and Walker conjecture only for complete domains of characteristic p. The proof does not use Ulrich modules. It cites the companion counterexample, result 195, only to show that approaches needing a finitely generated Cohen–Macaulay module over every ring cannot work everywhere. Our examples are small rings over the rational numbers; they illustrate the definitions, not the new theorem.

2:59How the proof goes

First, tidy up: complete both rings, make the fibre a single fat point, split R into irreducible pieces, and enlarge the residue field. Then factor the map through a ring T, which is R with extra smooth directions added, so T has the same multiplicity as R, and S is a quotient of T. Flatness gives S a short free resolution over T, and combining it with a Koszul complex on parameters gives a short chain of matrices whose cokernel encodes the multiplicity of S. The engine is a new uniform estimate. If every matrix entry of such a chain is divisible to order s, its cokernel must be at least about s^h times a fixed unit of size, up to a relative error of order 1/s, uniformly in the ring and in the ruler used to measure size. Its simplest case, in the plane: two curves that each vanish to order s at a point meet there at least about s² times; classically, at least s², as our examples illustrate. The paper proves the general case by blowing up the point and twisting by a vector bundle built by Eisenbud and Schreyer, with its cohomological roots placed near s times the roots of the derivative of (x+1)(x+2)⋯(x+h). That placement makes every layer sum share the same leading term, (h−1)! times s^h; our numerics agree. Then the entries are made deep. In characteristic p, Frobenius raises every entry to a high power for free; measured on the perfection, the cokernel’s size becomes a Hilbert–Kunz multiplicity, which by Ma’s identity gives e(S), and on each piece of T it is at least the ordinary multiplicity, so e(S) is at least e(R). In mixed characteristic there is no Frobenius: the paper adjoins roots of parameters, uses Heitmann’s Briançon–Skoda theorem, and measures with perfectoid lengths, taking two limits in a careful order. In characteristic zero, a counterexample would be encoded as finitely many polynomial equations; Artin approximation and reduction modulo a prime would turn it into a characteristic p counterexample, which cannot exist.

5:15Where it stands

The preprint is unrefereed and has not been revised. OpenAI’s Lean files are large, 278 files and about 54,000 lines, with no gaps we could find by search. But the statement they check is the supporting characteristic p result about Dutta multiplicity, not Lech’s inequality itself; they also contain the paper’s uniform estimate, as an internal lemma. We did not run the check. The collection’s formalization catalog does not list it. The paper is not among those OSVerify reviewed, and we have seen no expert review. If it holds, multiplicity never drops along a flat map of local rings, in any dimension and any characteristic: the total space of a flat family is always at least as singular as the point below it, as measured by multiplicity.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.