Serres Multiplicity Conjecture

### What is the conjecture

For a regular local ring $R$ with maximal ideal $\mathfrak{m}$, let $M$ and $N$ be finite $R$-modules with $\dim M + \dim N = \dim R$. The intersection multiplicity $\chi(M,N)$ defined via Tor functors is strictly positive: $\chi(M,N) > 0$.

**Sources:**
- https://en.wikipedia.org/wiki/Serre%27s_multiplicity_conjectures, https://arxiv.org/abs/1510.05146, https://www.cambridge.org/core/journals/compositio-mathematica/article/positivity-of-intersection-multiplicities-and-symbolic-powers-of-prime-ideals/4BB70FCBFA3B3D055EF322BB199D30E5

### Prerequisites needed

**Formalizability Rating:** 4/5 (as of 2026-01-20)

Mathlib has basic ring and module theory infrastructure, but formalizing Serre's conjecture requires significant development. Key missing pieces include: (1) formal Tor functor definitions and their properties, (2) intersection multiplicity theory via homological algebra, (3) dimension theory for modules over local rings, and (4) specialized properties of regular local rings. The conjecture sits at the intersection of commutative algebra and homological algebra, requiring substantial new theory beyond current Mathlib coverage.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-13
* ams-14
* ams-18

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Created by AI, reviewed by me.

Start with the conjecture statement and the cited sources, then assess the listed gaps in Tor functors, intersection multiplicity, module dimension theory, and regular local rings. Done would mean adding a formalized Serre Multiplicity Conjecture to the repository, but the issue indicates that substantial supporting theory is currently missing.

Written by the indexing model from the issue text.