A problem of Andrews and Dhar on partitions

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.

arXiv commentThis paper is motivated by the question: Can an AI system help discover and certify an explicit bijection between complicated combinatorial sets already known to be equinumerous?