Serre's positivity conjecture for intersection multiplicities
From OpenAI Aftermath
Serre's positivity conjecture for intersection multiplicities asserts that, over a regular local ring R, two nonzero finitely generated modules M and N with M ⊗ N of finite length and dim M + dim N = dim R have strictly positive intersection multiplicity χ(M, N), the alternating sum of the lengths of Tori(M, N). A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 23 September 2026, claims the conjecture in full, including ramified mixed characteristic. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Serre's reduction to the diagonal proves positivity in equal characteristic and in the unramified case, and also for formal power series rings over any complete discrete valuation ring. Roberts and, independently, Gillet and Soulé proved the vanishing conjecture, and Gabber proved nonnegativity in the remaining mixed-characteristic case using alterations.
- In ramified mixed characteristic, Skalit proved positivity for regular local rings essentially smooth over a two-dimensional regular local base, and KC and Soto Levins proved it for modules satisfying a Serre-liftability condition.
- The manuscript records, in a footnote, a December 2025 public post credited to Editan, Copilot and Gemini that also asserts the prime-quotient form of the conjecture, as a same-scope claim and not as an established theorem.
The original result
- Claim. Theorem 1.1 of Positivity of Serre's intersection multiplicity states that for every commutative Noetherian regular local ring R and nonzero finitely generated modules M, N with M ⊗R N of finite length and dim M + dim N = dim R, one has χR(M, N) > 0, with no restriction on characteristic or ramification and no liftability assumption.
- Method, as described: the proof combines normalized-length methods from almost mathematics (Faltings, Gabber–Ramero) and the perfectoid length results of Cai, Lee, Ma, Schwede and Tucker with descent properties of algebraic K-theory.
- Source. The manuscript Positivity of Serre's intersection multiplicity at commit
1581d4c. - Formalization. The collection lists no Lean formalization for this result.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Session note of 7 October 2026, section 5, in the GitHub repository eliottcassidy2000/math | Remark (reading) | Summarizes the cases of positivity known before the manuscript and locates its new content in ramified mixed characteristic with ring dimension at least five and a prime quotient of dimension at least three, a correction recorded after the session's own audit. It finds no application to the session's research problems and records the result as a guardrail. | A note in a multi-agent AI research repository, which states that the OpenAI results were accepted as correct by its owner's directive. |
| 2026-10-07 | unaoya/SerrePositivity (GitHub) | Formalization (in progress) | An early-stage Lean 4 formalization of the manuscript. Theorem 1.1 and the core case are stated with proofs left as sorry, together with a skeleton of the core-case data. The plan is to formalize the paper-specific argument first, to state the paper's new general theorems and the literature inputs as named axioms, and to reach a derivation of Theorem 1.1 whose only axioms are these named hypotheses. |
GitHub repository, early stage. The README states that it is not affiliated with OpenAI. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_261 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. The reviewer states that it read all five sections in full and checked the main steps in detail, but did not verify the mixed-characteristic perfectoid inputs cited from Cai, Lee, Ma, Schwede and Tucker or the precise hypotheses of the Land–Tamme coefficient descent used for a non-Noetherian coefficient algebra. Its two minor notes are that the whole argument rests on one K-theoretic descent input with such a coefficient algebra, whose individual steps it found formally sound, and a consistency test of the descent statement on the Dutta–Hochster–McLaughlin ring, which found no contradiction. | Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The vanishing, nonnegativity and earlier positivity results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
