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:
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.
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link
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:
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:
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
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link