The Address Before the Room

In 1748, Euler proved something that feels like a magic trick. Take a positive integer $n$. Count the ways to write $n$ as a sum of distinct positive integers. Then count the ways to write $n$ as a sum of odd positive integers, where repetitions are allowed. The two answers are always the same.

For $n = 8$, the partitions into distinct parts are

$8, \quad 7+1,$ $\quad 6+2,$ $\quad 5+3,$ $\quad 5+2+1,$ $\quad 4+3+1.$

The partitions into odd parts are

$7+1, \quad 5+3,$ $\quad 5+1+1+1,$ $\quad 3+3+1+1,$ $\quad 3+1+1+1+1+1,$ $\quad 1+1+1+1+1+1+1+1.$

Six and six. Euler proved that this coincidence always happens.

The proof that counts, and the proof that explains

This coincidence holds for every $n$, and we are interested in two proofs of it. Euler’s proof is a small miracle of cancellation. If $d(n)$ counts the number of partitions of $n$ into distinct parts, then we have the generating function

$\sum\limits_{n\ge 0}d(n) q^n$ $= \prod\limits_{m \ge 1} (1 + q^m)$ $= 1 + q + q^2 + 2q^3$ $+ 2q^4 + 3q^5 + 4q^6$ $+ 5q^7 + 6q^8 + \cdots$

The reason is simple: in the factor $(1 + q^m)$, we either choose the part $m$ once, contributing $q^m$, or do not choose it, contributing $1$. Multiplying over positive integers $m$ records every partition into distinct parts exactly once.

If $o(n)$ counts the partitions of $n$ into odd parts, which can be repeated, the same thinking gives

$\sum\limits_{n\ge 0}o(n) q^n$ $= \prod\limits_{m\ge 1}\left(1 + q^{2m-1} + q^{2(2m-1)} + q^{3(2m-1)} + \cdots \right)$ $= \prod\limits_{m\ge 1}\dfrac{1}{1 - q^{2m-1}}$ $= 1 + q + q^2 + 2q^3 + 2q^4 + 3q^5$ $+ 4q^6 + 5q^7 + 6q^8 + \cdots$

Since parts might repeat, we need to use the geometric series identity

\[1 + x + x^2 + x^3 + \cdots = \dfrac{1}{1-x}, \quad |x| < 1.\]

We take $x=q^{2m-1}$, which is valid as a formal power series (or for $|q|<1$).

Euler’s Theorem tells us that $d(n)=o(n)$ for every integer $n$, and one proof is given by the identity

$\sum\limits_{n\ge 0}d(n) q^n$ $= \prod\limits_{m\ge 1} 1 + q^m)$ $= \dfrac{\prod\limits_{m\ge 1}(1 - q^{2m})}{\prod\limits_{m\ge 1}(1 - q^m)}$ $= \prod\limits_{m\ge 1}\dfrac{1}{1 - q^{2m-1}}$ $= \sum\limits_{n\ge 0}o(n) q^n,$

where, in the infinite product in the middle, the even factors in the numerator cancel the even factors in the denominator, leaving only the odd denominators.

However, a generating function by itself doesn’t clarify everything; it merely shows that two lists of numbers (i.e., in this case the coefficients $d(n)$ and $o(n)$) are the same. The challenge is to find a 1-1 matching. In combinatorics, such bijections provide a direct, structural explanation: every single object in the first family is paired with exactly one unique object in the second, and vice versa. It shows why the counts match.

An elegant bijection is known, and it turns out to just be carrying in base two. Start with a partition into odd parts, such as

\[9+9+9+9+5+5+5+1+1.\]

Pair equal parts. Two 9’s make 18, and two 18’s make 36. Two 5’s make 10, with one 5 left over. Two 1’s make 2. So

$9+9+9+9$ $+5+5+5+1+1$ $\longmapsto 36+10+5+2.$

No part repeats. The reason is binary: each odd part produces at most one $r$, one $2r$, one $4r$, one $8r$, and so on. Different odd parts cannot collide, because every positive integer has a unique odd core after all factors of $2$ are removed.

The inverse is just as simple: split every even part in half until only odd parts remain. This recovers the original partition, so the matching goes both ways.

This is our happy moment. The algebra proves equality. The bijection reveals the hidden matching that explains why the counts match.

A beastly descendant of Euler

Euler’s theorem is the $m = 2$ case of a broader result usually called Glaisher’s partition theorem. In Glaisher’s theorem, powers of two are replaced by powers of $m$, and the same carrying idea explains why two partition families have the same size.

In December 2025, George Andrews and Debajyoti Dhar found a striking companion to Glaisher’s extension of Euler’s theorem. In their identity, a largest-part condition on one side becomes a smallest-part condition on the other side. Their cubic case is especially intriguing.

They define a family $C_3(n)$ of partitions whose largest part is divisible by $3$, say $3J$, and whose parts at most $J$ occur at most twice. They also define a family $D_3(n)$ of partitions into nonnegative parts whose smallest part occurs exactly three times and whose larger parts occur at most twice.

For example, $(9,4,1,1)$ lies in $C_3(15)$: its largest part is $9 = 3 \times 3$, and the parts at most 3 occur at most twice. On the $D_3$ side, $(4,3,3,2,1,1,1)$ is allowed: its smallest part 1 occurs exactly three times, while the larger parts 4,3,3, and 2 occur at most twice.

Andrews and Dhar proved analytically, for nonexceptional $n$, that

\[|C_3(n)| = |D_3(n)|/3.\]

The exceptional values are the integers that are one more than a triangular number, $T_r + 1$, where $T_r = r(r+1)/2$. Apart from these values, the formula says that the $C_3$ objects match exactly one third of the $D_3$ objects.

Their proof is much more complex than Euler’s straightforward proof. It involves analyzing the case where $m=3$ of a series of complicated steps given below, which is really only understandable by experts. See their paper for the details and the definitions of the symbols.

Andrews and Dhar asked for the Euler-style explanation: can one give a bijective proof?

Which third?

The denominator 3 creates a basic problem. A bijection cannot map $C_3(n)$ onto "one third of $D_3(n)$" until we decide which third we mean, if we can figure that out at all.

Our first step is to identify a canonical third by means of an equidistribution theorem. If $\mu$ is a partition in $D_3(n)$, let $\tau(\mu)$ be the number of parts strictly larger than the smallest part. Now sort the $D_3(n)$ objects into three classes according to $\tau(\mu)$ modulo 3:

\[D_3^{(0)}(n), \quad D_3^{(1)}(n), \quad D_3^{(2)}(n).\]

What the equidistribution theorem says, informally For every nonexceptional $n$, we prove that these three sets have equal size. Thus $D_3^{(0)}(n)$ is not an arbitrary third. It is a natural, canonical third selected by the statistic $\tau(\mu)$ modulo 3.

The proof uses a root-of-unity filter, a standard but elegant trick in generating functions. One introduces a variable that tracks $\tau(\mu)$, then substitutes a nontrivial cube root of unity. The three residue classes are weighted by these roots of unity. When $n$ is not one more than a triangular number, the proof shows that the nontrivial filters vanish, forcing the three residue classes to be equal.

A tiny complete example

The case $n = 6$ is small enough to see the answer. The $C_3$ objects are

\[(6), \quad (3,3), \quad (3,2,1).\]

On the $D_3$ side, the residue-zero condition selects exactly three objects:

\[(4,1,1,0,0,0), \quad (3,2,1,0,0,0), \quad (2,2,2).\]

The problem is to find a general map that explains, just like Euler’s powers-of-two carrying trick, the Andrews-Dhar theorem not just for $n=6$, but all nonexceptional $n$.

The bijection is a machine

The map we construct is not a single move. It is a carefully engineered composition of four transformations:

Here is a loose description of the four pieces. Interested readers can find the details in the arXiv manuscript given at the end of this blog.

1. The finite Glaisher step. The map $\Gamma$ lowers one distinguished largest part $3J$ to $3J – 1$, then carries the remaining parts in base 3. The output is a partition into parts not divisible by 3 whose largest part is congruent to 2 modulo 3.

2. The inverse Stockhofe step. The map $\Phi_3^{-1}$ transforms a 3-regular partition into a 3-flat partition. Here 3-regular means no part is divisible by 3. A 3-flat partition has no steep drops: every consecutive gap is 0, 1, or 2.

3. Conjugation. This is the ‘ map above. Reflect the Ferrers diagram, a staircase visualization of the partition, across its diagonal. This standard operation turns multiplicity restrictions into gap restrictions, and vice versa.

4. The smallest-part raising step. The final map $T$ adjusts the bottom of the partition so that the smallest part occurs exactly three times and the residue condition $\tau(\mu)\equiv 0\pmod{3}$ is satisfied.

Each step has a natural inverse. Taken together, and in this very particular order, they give a bijection

\[\iota_n : C_3(n) \to D_3^{(0)}(n)\]

for every $n\geq 1$. Once the equidistribution theorem identifies $D_3^{(0)}(n)$ as one of three equal classes in the nonexceptional cases, this answers the Andrews-Dhar question.

If you’re feeling adventurous, take a moment to enjoy the bijection worked out explicitly for $n=15$ in the table below. If the bijection does not look easy from the table, that is exactly the point.

The AxiomProver story

This project was motivated by a broader question about AI-assisted mathematics: can an AI system help move us from "this theorem is true" to "this theorem has a good explanation”. This research reveals underlying structure that enriches our understanding of these partitions.

AxiomProver played two distinct roles. First, it autonomously produced and Lean-verified the residue-class equidistribution theorem, the result that explains why the $D_3$ objects split into three equal classes in the nonexceptional cases.

Second, the bijection itself was found through human-AxiomProver collaboration. The final map was organized as a composition of four component bijections, and the Lean verification was split accordingly: one run for the equidistribution theorem and further runs for the components of the bijection.

The formalization used Lean 4.28.0. For the runs corresponding to the equidistribution theorem and the first three bijective components, AxiomProver generated both the problem statements and the machine-checked solution files. For the final Stockhofe component, AxiomProver produced the formal problem statement and a structurally complete solution assuming the relevant Stockhofe-type result; a human author completed the final repository file.

That division of labor is important. We did not merely ask a system to rubber-stamp a finished proof. The formal runs helped clarify what the intermediate sets should be, how the maps should be organized, and where the hard bookkeeping lived. In a problem about finding the hidden matching behind a generating-function identity, the machine helped expose the architecture of the matching.

Why this matters

Euler’s theorem teaches a lesson that still guides partition theory. A generating function can prove that two sequences agree. A bijection explains much more; it offers insight and a deeper understanding.

For Euler, the explanation fits in a sentence: bundle odd parts in powers of two. For Andrews and Dhar, the explanation is a machine: carry, flatten, reflect, and raise. The result is a direct matching between $C_3(n)$ and the canonical third $D_3^{(0)}(n)$.

That is the combinatorial payoff. The identity is no longer a crazy gymnastics event involving generating functions. It becomes a reversible structure, object by object.

This is also the larger promise of AI in research mathematics. We want systems that do more than check the final line. We want tools that help uncover the hidden structures that make theorems intelligible.

From Euler’s powers of two to AxiomProver’s Lean files, the goal is the same: turn equality into explanation. As a fitting ending, we share a screenshot of the e-mail K.O. received from George Andrews in response to this paper.

Paper and code

Paper: A problem of Andrews and Dhar on partitions, by Simon Mahns, Ken Ono, and Jujian Zhang.

arXiv: https://arxiv.org/abs/2606.05117

Code repository: https://github.com/AxiomMath/andrews_dhar_problem