OpenAI claim summary for Math-2193
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
Taking $M=R/P$ and $N=R/Q$ in the general finite-module positivity theorem proves the prime-ideal formulation when the intersection has finite length and the dimensions are complementary. The separate multiplicity-product refinement requires its additional tangent-cone dimension hypothesis.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Serre's Positivity Conjecture
OpenAI's claim
OpenAI presents a mathematical result relevant to this question in the selected manuscript. Serre intersection numbers are claimed to be positive when two nonzero finite modules have complementary support dimensions and a finite-length tensor product over a regular local ring, even in ramified mixed characteristic.Mathematical statement of the claimed result
Result 1.
Take nonzero finite modules $M,N$ over a local ring $(R,\mathfrak m)$ which is Noetherian and regular, with $\dim R=d$. Here finite means finitely generated. Define \[ \chi^R(M,N)=\sum_{i\ge0}(-1)^i\operatorname{length}_R\operatorname{Tor}^R_i(M,N). \] The source asserts \[ \operatorname{length}_R(M\otimes_RN)<\infty,\quad \dim_RM+\dim_RN=d\quad\Longrightarrow\quad\chi^R(M,N)>0. \] A separate corollary, for primes $P,Q$ in a regular local ring $A$, assumes finite length of $A/(P+Q)$, complementary dimensions, and \[ T=\operatorname{gr}(A/P)\otimes_{\operatorname{gr}A}\operatorname{gr}(A/Q),\qquad\dim T\le1. \] It then gives $\chi^A(A/P,A/Q)\ge e_{\mathfrak m}(A/P)e_{\mathfrak m}(A/Q)$, with equality precisely when $\dim T=0$. Here the graded rings use maximal-ideal filtrations and $e_{\mathfrak m}$ denotes Hilbert--Samuel multiplicity.Outline of the argument
The reductions pass to completed quotient domains and algebras carrying normalized length. Galois-averaged supported K-theory compares ordinary Tor Euler numbers with normalized ones; parameter Koszul exactness and truncated finite resolutions then force each relevant normalized contribution to be positive.Formal verification
Family 193 has no Lean scope page in this release. Its selected result is not presented as formalized. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.Status caveat
OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.Sources
- OpenAI, Positivity of Serre's Intersection Multiplicity, 2026-09-23; citation key
OAI:Positivity-of-Serres-Intersection-Multiplicity-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main; Statement source: cor:tangent-cone. - OpenAI catalogue entry.