Monomial Conjecture

### What is the conjecture

For a Noetherian local ring of Krull dimension $d$ with a system of parameters $x_1, \ldots, x_d$, the monomial conjecture states that for all integers $t \geq 0$, the monomial product $x_1^t x_2^t \cdots x_d^t$ does not belong to the ideal generated by the $(t+1)$-powers: $$x_1^t x_2^t \cdots x_d^t \notin (x_1^{t+1}, \ldots, x_d^{t+1})$$

**Sources:**
- https://en.wikipedia.org/wiki/Monomial_conjecture, https://www.math.utah.edu/~roberts/armc.pdf, https://www.math.utah.edu/vigre/minicourses/algebra/hochster.pdf

### Prerequisites needed

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

The core concepts of Noetherian local rings, Krull dimension, systems of parameters, and ideal membership are foundational in Mathlib's commutative algebra library. However, formalizing this conjecture requires significant development of the theory of Noetherian local rings, depth, and their properties. Additional infrastructure for working with monomial ideals and systems of parameters in their full generality would need to be established or extended.

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

* ams-13
* ams-16
* ams-14

### 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.