Kazhdan-Lusztig conjecture

### What is the conjecture

The Kazhdan–Lusztig conjecture relates the composition series of Verma modules in Category $\mathcal{O}$ to Kazhdan–Lusztig polynomials. Let $W$ be a Coxeter group (e.g., the Weyl group of a reductive Lie group). For each $w \in W$, let $M_{w \cdot 0}$ denote the Verma module with highest weight $w \cdot 0$ and $L_{w \cdot 0}$ the simple module with highest weight $w \cdot 0$ in the principal block of Category $\mathcal{O}$. The conjecture states that for $w, w' \in W$, the multiplicity of $L_{w \cdot 0}$ in the Jordan-Hölder composition series of $M_{w' \cdot 0}$ is given by evaluating the Kazhdan–Lusztig polynomial $P_{w',w}(q)$ at $q = 1$:

$$[M_{w' \cdot 0} : L_{w \cdot 0}] = P_{w',w}(1)$$

where the Kazhdan–Lusztig polynomials are defined recursively in terms of the Hecke algebra associated to $W$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Kazhdan%E2%80%93Lusztig_polynomial; https://ncatlab.org/nlab/show/Kazhdan-Lusztig+theory; https://yisun.io/notes/klconj.pdf; https://windshower.github.io/linchen/teaching/s2024/lecture8.pdf; https://www.numdam.org/article/ASENS_1981_4_14_3_261_0.pdf

### Prerequisites needed

**Formalizability Rating:** 5/5 (0 is best) (as of 2026-03-14)

Building blocks (1-3; from search results):
- Coxeter groups and Weyl groups (partial support in Mathlib for basic group operations, but not Coxeter-specific theory)
- Modules and composition series (basic infrastructure exists in Mathlib)
- Polynomial rings (polynomial.lean in Mathlib)

Missing pieces (exactly 2; unclear/absent from search results):
- Hecke algebras and Kazhdan-Lusztig polynomials (not in Mathlib; would require defining the recursive formula and establishing key properties)
- Category $\mathcal{O}$, Verma modules, and the representation theory framework (not in Mathlib; requires development of BGG theory and highest weight representations)

Rating justification (1-2 sentences): The statement requires formalizing Hecke algebras and Kazhdan-Lusztig polynomials as a new theory, along with the specialized representation-theoretic category $\mathcal{O}$ and Verma modules. While basic building blocks (groups, modules, polynomials) exist in Mathlib, the specific infrastructure needed (Hecke algebras, KL polynomials, BGG theory) requires significant new development.

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

* ams-20
* ams-17
* ams-05

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

---
This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)