Kronecker Coefficient Combinatorial Interpretation Conjecture

### What is the conjecture

The **Kronecker coefficient** $g(\lambda, \mu, \nu)$ for partitions $\lambda, \mu, \nu$ is the multiplicity of the irreducible representation $S^\nu$ of the symmetric group $S_n$ in the tensor product $S^\lambda \otimes S^\mu$ of two irreducible representations.

**Conjecture (Murnaghan, 1938):** There exists a family of combinatorial objects $\mathcal{O}_{\lambda,\mu,\nu}$ such that
$$g(\lambda, \mu, \nu) = |\mathcal{O}_{\lambda,\mu,\nu}|$$

In other words, find a direct combinatorial interpretation (positive combinatorial formula) for the Kronecker coefficients. This remains one of the most important unsolved problems in algebraic combinatorics.

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

**Sources:**
- - [Wikipedia: Kronecker coefficient](https://en.wikipedia.org/wiki/Kronecker_coefficient)
- [Panova, Greta. Kronecker coefficients: combinatorics, complexity and beyond. 2017.](https://www.math.ucla.edu/~pak/hidden/papers/Panova_Porto_meeting.pdf)
- [arXiv:2511.02312 - A combinatorial interpretation for certain plethysm and Kronecker coefficients](https://arxiv.org/abs/2511.02312)
- [Simons Institute - Combinatorics and Complexity of Kronecker Coefficients](https://simons.berkeley.edu/talks/combinatorics-complexity-kronecker-coefficients)
- [AIM Workshop: Combinatorics and Complexity of Kronecker Coefficients](https://aimath.org/pastworkshops/kroncoeffrep.pdf)

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-02-15)

Building blocks (from Mathlib):
- `Partition` (order-theoretic in Mathlib.Order.Partition.Basic; integer partitions may be available elsewhere or need definition)
- `Representation` (basic group representation infrastructure in Mathlib.GroupTheory)
- `TensorProduct` (module tensor products in Mathlib.LinearAlgebra)

Missing pieces:
- Character theory for symmetric groups and definition of Kronecker coefficients via character inner products
- Formalization of "combinatorial family parameterized by (λ,μ,ν) with cardinality equal to g(λ,μ,ν)"

Rating justification: The basic objects (partitions, representations, tensor products) have some Mathlib support, but the Kronecker coefficient itself is defined via character theory, which requires substantial infrastructure around symmetric group characters. Additionally, formalizing the existential claim about combinatorial families adds another layer of abstraction not immediately available.

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

* ams-05
* ams-20

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

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)