Representation theory is often introduced as the study of symmetry through linear algebra. Its formulas can look abstract, and its objects can feel far removed from pictures. But our new paper with Rekha Biswal tells a more visual story: some multiplicity numbers from representation theory are secretly governed by paths that climb, descend, and stay below a fixed ceiling. The paper also served as a test case for AxiomProver, the automated reasoning system we are developing at Axiom Math. Starting from natural-language theorem statements, AxiomProver autonomously produced Lean/Mathlib-verified proofs of the theorems in the paper. This blog explains the human mathematical story behind those formal proof artifacts.
Here is a tiny example of the kind of expression that appears in the paper. One of the numbers we want is the coefficient of $x^4$ in the power series expansion of the rational function
\[p_2(x) / p_4(x),\]
where the $p_r(x)$ are the Chebyshev polynomials defined by the recurrence relation
\[p_{r+1}(x) = p_r(x) - x\,p_{r-1}(x),\]
with $p_0(x) = p_1(x) = 1$. For those reading the paper who want the representation-theoretic labels, this example corresponds to $m = 4,\ \xi = (1, 1, \ldots, 1)$, with nine parts, and target weight $\mu = 1.$. The recurrence gives
\[p_2(x) = 1 - x,\quad p_3(x) = 1 - 2x,\quad p_4(x) = 1 - 3x + x^2,\]
and expanding the quotient as a power series gives
\[p_2(x) / p_4(x) = (1 - x)/(1 - 3x + x^2) = 1 + 2x + 5x^2 + 13x^3 + 34x^4 + \cdots .\]
While the coefficient for $x^4$ is $34$, the formula itself presents a puzzle: it is full of subtractions and potential cancellations. One might wonder why a positive integer arises from a quotient whose terms are not positive.
This very number, $34$, turns out to be a tally of natural combinatorial structures called Dyck paths. This is the main transformation of the paper, illustrated by a single example: a value that initially appears to be the byproduct of algebraic cancellation in a rational function is, within specific families, shown to be an honest count of combinatorial objects.
The example is deliberately small, but the two bridges behind it are not. First, representation theory must be connected to these rational functions in the first place; that is a deep structural step. Second, these quotients must then be connected to objects one can count; that is the new combinatorial step in our paper. We will not unpack those bridges here, but they are the reason the simple-looking quotient carries meaningful representation-theoretic information.
These are the paper’s central points. From representation theory, we are led to infinite families of rational functions called Chebyshev quotients. Their coefficients are not random. We prove that, after the evident cancellations, each quotient either becomes a polynomial and eventually stops, or else its sufficiently late coefficients are strictly positive. In important families, the explanation becomes even more concrete: the coefficients count Dyck paths.
Where the quotient comes from
Representation theory often asks how a complicated object decomposes into standard pieces. The answer is encoded in multiplicities: numbers recording how often a particular piece occurs.
The multiplicities in this paper come from a part of representation theory built around the Lie algebra $sl_2$. A Lie algebra is a linear-algebraic way of studying infinitesimal symmetries: it records how continuous symmetries behave when viewed very close to the identity. Just as a tangent line captures the local direction of a curve, a Lie algebra captures the local directions in which a continuous symmetry can change. The algebra $sl_2$ is one of the smallest and most important examples, and its current-algebra version $sl_2[t]$ allows those symmetries to vary with a polynomial parameter $t$.
You do not need the details to follow the story. What matters here is that this representation theory produces multiplicity numbers, known as Demazure multiplicities, and Chebyshev quotients turn these numbers into coefficients like the one above. These multiplicities are not just bookkeeping. To representation theorists, Demazure multiplicities describe how complicated modules are assembled from important standard pieces. Understanding them turns an abstract decomposition into something computable, visual, and sometimes combinatorial.
This translation changes the problem in a useful way. Instead of trying to see the multiplicities directly inside the technical representation theory, we can look at the power-series coefficients of rational functions built from a very simple recurrence. The surprise is that these quotients contain minus signs, so positivity is not visible term by term. The main question becomes: what hidden structure makes the final coefficients positive?
The theorem in plain English
The first main result in the paper gives a clean dichotomy. Once the obvious common factors are removed, a Chebyshev quotient from this setup behaves in one of two ways.
First, it can become a polynomial. Then its coefficient sequence eventually ends.
Second, it can remain genuinely infinite. In that case, all sufficiently late coefficients are strictly positive.
The proof uses the smallest positive root of the denominator to control the long-term behavior of the coefficient sequence, unless the denominator disappears through cancellation.
This proves that eventual positivity has a reason. But it does not yet tell us what the coefficients are counting. For that, the paper turns to combinatorics.
Why cancellation appears
The first combinatorial explanation does not yield a clear positive count. The polynomials $p_r(x)$ have a natural interpretation in terms of matchings: collections of edges in a path graph with no shared endpoints. These matching terms appear with alternating signs.
The reciprocal factors have a different interpretation. They count bounded strip walks: paths that move up or down by one step while staying between a floor and a ceiling.
Putting these two interpretations together, each coefficient becomes a signed count involving matchings and bounded walks. That is already concrete, but it still allows cancellation. Some objects contribute positively, and some contribute negatively.
How the signs disappear
In several natural infinite families, the quotient factors in just the right way. Each factor becomes the generating function for bounded Dyck paths.
A Dyck path is a path that starts on the ground, uses up-steps and down-steps, never goes below the ground, and returns to the ground. A bounded Dyck path also has a ceiling. This is the friendliest object in the story: something one can draw on graph paper.
The key bijection is simple. Start with a walk inside a bounded strip. Add a prescribed block of up-steps at the beginning and a prescribed block of down-steps at the end. The result is a bounded Dyck path.
This is the satisfying moment in the story. A multiplicity from representation theory becomes a coefficient of a rational function. The rational function appears to involve cancellation. But in these families, the cancellation has a hidden explanation: the coefficient is actually counting tuples of bounded Dyck paths.
Where the Dyck-path models appear
The paper proves this unsigned path interpretation for three broad families of examples. Roughly speaking, these are cases where the algebraic quotient factors into pieces that each have their own path interpretation.
The exact hypotheses matter in the theorem statements, but the main message is simple: in these families, positivity is not merely a consequence of a limiting argument. It is positive because it counts actual bounded Dyck paths.
The point is not that every Chebyshev quotient automatically has a Dyck-path model. The paper is careful about this. The general theorem gives eventual positivity and a signed matching-and-walk formula. The stronger unsigned Dyck-path interpretation is proved for natural families in which the quotient factors as needed.
Why this matters
A formula with cancellations can be hard to trust and hard to interpret. A path model is different. It gives a concrete set of objects whose size is the number one wanted to compute.
That is why the result is useful. It turns numerical Demazure multiplicities from mysterious coefficients into quantities with visible combinatorial meaning. It also separates what is general from what is special: eventual positivity holds broadly, a signed matching-and-walk interpretation explains the coefficients in this setup, and bounded Dyck paths give clean unsigned models in important families.
There is also a natural next question. Earlier work gave a different Dyck-path model for graded multiplicities, including a statistic that remembers the grading. For the path model introduced here, the right statistic for the full q-dependent graded multiplicities is not yet known. Finding it would be an interesting continuation of the story.
A little history: Lie and Demazure
This subject reaches back to two major figures. Sophus Lie gave mathematics one of its central languages for the study of continuous symmetry. Michel Demazure helped shape modern algebraic geometry and representation theory, including the modules and operators that now bear his name.
Image credits
Sophus Lie (1842-1899) was a Norwegian mathematician whose work led to Lie groups and Lie algebras, structures now central in geometry, differential equations, representation theory, and mathematical physics.
Michel Demazure (born 1937) is a French mathematician whose work has influenced algebraic geometry, algebraic groups, and representation theory. He was a member of Nicolas Bourbaki, the famous collective that wrote under a single name in an ambitious effort to reorganize modern mathematics with exceptional precision. Demazure also co-authored the SGA 3 volumes, Schémas en groupes, with Alexandre Grothendieck; SGA stands for Séminaire de Géométrie Algébrique du Bois Marie.
The AxiomProver story
The paper also has an AI component. The surprising second story is that, in the paper, we report that AxiomProver produced and verified Lean/Mathlib proofs from natural-language theorem statements. The paper, written without AI, then explains what those formal proof artifacts mean mathematically: why Chebyshev quotients appear, why positivity eventually holds, and why bounded Dyck paths emerge in natural families.
Lean proofs are not written like ordinary mathematical exposition. They make bookkeeping explicit: rewrites, coercions, side conditions, and case splits. That is exactly what makes them valuable as proof artifacts, but it also means that a human-readable paper still has to reconstruct the conceptual route through the argument.
In this project, the formal proof and the expository paper play complementary roles. The Lean files provide machine-checked verification. The paper and this blog provide the mathematical story.
Paper and code
Paper: Chebyshev quotients, Demazure multiplicities, and Dyck-path models, by Rekha Biswal, Ken Ono, and Jujian Zhang.
arXiv: https://arxiv.org/abs/2604.25246
Code repository: https://github.com/AxiomMath/Biswal
Advances in Applied Mathematics: https://www.sciencedirect.com/science/article/abs/pii/S0196885826000874