A problem of Andrews and Dhar on partitions
Simon Mahns, Ken Ono, Jujian Zhang
math.CO
Jun 3, 2026 · v1
TL;DR
AxiomProver autonomously generated and Lean-verified a residue-class equidistribution theorem and autoformalized the partition bijection proof.
Abstract
This paper is motivated by a broad question about AI-assisted mathematics: can an AI system help discover and certify an explicit bijection between two infinite sequences of complicated combinatorial sets already known to be equinumerous? The challenge is to find a reversible structure explaining that equality uniformly across the sequence. We give an affirmative test case in the setting of a partition problem. Andrews and Dhar introduced two partition families $\mathcal{C}_3(n)$ and $\mathcal{D}_3(n)$, and for "nonexceptional'' $n$, they asked for a bijective proof of their equality \[ |\mathcal{C}_3(n)|=\frac{|\mathcal{D}_3(n)|}{3}. \] We prove a residue-class equidistribution theorehm for $\mathcal{D}_3(n)$ that identifies a "canonical third'' subset $\mathcal{D}_3^{(0)}(n)\subseteq \mathcal{D}_3(n)$. Answering their question, we construct a bijection \[ ι_n:\mathcal{C}_3(n)\longrightarrow \mathcal{D}_3^{(0)}(n) \] as a highly structured composition of four maps. AxiomProver autonomously produced and Lean-verified the equidistribution theorem. The bijection was found through human--AxiomProver collaboration, and the theorem was autoformalized and verified by the system.
Problem
Andrews and Dhar defined two partition families C_3(n) and D_3(n) and proved |C_3(n)| = |D_3(n)|/3 for nonexceptional n, but asked for a bijective proof explaining this equality.
Approach
The authors prove a residue-class equidistribution theorem showing D_3(n) splits into three equal-size classes indexed by a statistic tau modulo 3. They then construct an explicit bijection from C_3(n) to the residue-zero class as a composition of four maps: a finite Glaisher carrying step, an inverse bridge map, conjugation, and a tail-adjustment. AxiomProver (an AI system) autonomously generated and Lean-verified the equidistribution theorem, and the bijection was discovered through human-AI collaboration and autoformalized in Lean 4.
Results
The bijection answering the Andrews-Dhar problem is constructed and formally verified in Lean 4.28.0. AxiomProver independently produced the equidistribution theorem proof and verified all four component bijections in separate parallel runs.
