A proof of the Theta conjecture
Haojun Bai, Feng Gu, Zhuowei Lin, Dun Qiu, Minhao Zhang
math.CO
Nov 9, 2026 · v1
TL;DR
The main theorem (touching refinement of the Theta conjecture, Theorem 1.4) is formalized in Lean 4, with a public GitHub repository.
Abstract
We prove the touching refinement of the Theta conjecture of Interdonato and Iraci, giving a formula for $Θ_{e_\ell}Θ_{e_k}\nabla E_{d,j}$ as a weighted sum over parking functions with decorated rises and valleys and touch number $j$. Summing over $j$ gives the Theta conjecture. As corollaries, we prove the valley Delta conjecture of Haglund, Remmel, and Wilson and its generalized version proposed by Qiu and Wilson. Our proof compares algebraic and combinatorial recurrences using an extension of the plethystic substitution $X\mapsto(q-1)X$ to quasisymmetric functions. The algebraic recurrence follows from an endomorphism constructed by D'Adderio, Interdonato, Iraci and Pagaria on the Dyck path algebra of Carlsson and Mellit. The combinatorial recurrence is obtained by introducing signed labels and deleting the main diagonal. The two recurrences have the same initial conditions, which identifies the corresponding generating functions.
Problem
The Theta conjecture of Interdonato and Iraci, in its touching refinement, gives a combinatorial formula for Θ_{e_ℓ}Θ_{e_k}∇E_{d,j} as a weighted sum over parking functions with decorated rises and valleys and touch number j. The valley Delta conjecture and its generalized version are special cases.
Approach
The proof compares an algebraic recurrence with a combinatorial recurrence, using an extension of the plethystic substitution X↦(q−1)X to quasisymmetric functions. The algebraic recurrence comes from an endomorphism of the Carlsson–Mellit Dyck path algebra constructed by D'Adderio, Interdonato, Iraci and Pagaria. The combinatorial recurrence is obtained by introducing signed labels and deleting the main diagonal of parking functions. The main theorem is also formalized in Lean 4.
Results
Both recurrences have the same initial conditions, which proves the touching refinement and hence the Theta conjecture. As corollaries, the valley Delta conjecture of Haglund–Remmel–Wilson and the generalized version of Qiu–Wilson follow. A Lean 4 formalization of Theorem 1.4 is publicly available.
