← All papers
First page of Leaving the Hall: explicit formulas for Neguţ operators

Leaving the Hall: explicit formulas for Neguţ operators

Michele D'Adderio, Giovanni Interdonato, Alessandro Iraci, Roberto Pagaria

math.CO Aug 14, 2026 · v1
Several finite algebraic identities underlying the Theta operator extension and part of the Theta conjecture proof were formalized in Lean, assisted by Aristotle.
Recent major breakthroughs in $q,t$-combinatorics include the introduction of the Dyck path algebra $\mathbb{A}_{q,t}$ by Carlsson and Mellit and of the Catalanimals by Blasiak et al., both of which led, among other things, to independent proofs of different extensions of the rational shuffle conjecture of Bergeron et al. The first main contribution of this paper is a simple, explicit formula inside the algebra $\mathbb{A}_{q,t}$ for the Neguţ operators, yielding a direct, elementary connection between the original operators of the rational shuffle conjecture and the corresponding Catalanimals. Our formula bypasses the elliptic Hall algebra, turning these operators into transparent, workable tools whose action we can compute exactly and efficiently on any symmetric function, not just constants. Our second main contribution consists of a series of explicit formulas relating the Neguţ operators to the Theta operators introduced by D'Adderio et al. To prove these formulas, we provide an extension of the aforementioned Theta operators to the entire algebra $\mathbb{A}_{q,t}$, allowing us to obtain a series of new combinatorial results. The algebraic computations underlying this extension have been formalized in Lean. To showcase the power of our results, we give a proof, also partially formalized in Lean, of the Theta conjecture of D'Adderio et al., first stated in 2019.

The Neguţ operators arising in q,t-combinatorics and the rational shuffle conjecture are usually described implicitly via the elliptic Hall algebra, making them hard to compute. The relationship between these operators and the Theta operators of D'Adderio et al. was not fully understood, and the Theta conjecture (2019) remained open.

Explicit formulas for the Neguţ operators are given inside the Dyck path (Carlsson–Mellit) algebra A_{q,t}, bypassing the elliptic Hall algebra. The Theta operators are extended to an endomorphism of the entire algebra A_{q,t}, and commutation relations with the Neguţ operators are derived. The finite algebraic identities underlying this extension were formalized in Lean using Harmonic's Aristotle, though the concrete symmetric-function action was not formalized.

Explicit, computationally efficient formulas relating Neguţ and Theta operators are obtained, yielding new combinatorial results. The Theta conjecture of D'Adderio et al. is proved, with the proof partially formalized in Lean.