Direct discovery · Mathematics

Human–AxiomProver collaboration constructs a bijection for the Andrews–Dhar partition problem

An explicit four-map bijection answering the cubic Andrews–Dhar partition question, with accompanying Lean artifacts.

Summary

The paper identifies a residue-zero subfamily and constructs a bijection to it through four partition maps. Authors describe collaborative discovery and separate Lean runs; a human completed the final Stockhofe component in the repository.

AI role

Generated a residue-class equidistribution proof and assisted guided search for the bijection and formalization of its components.

Narrative role

Adds a concrete case of AI assisting the construction of an explanatory mathematical map beyond proving equality of counts.

Caveat

Author-reported checking with public artifacts; this run did not independently build Lean or certify statement equivalence. The final component required human completion. The June paper date is distinct from its July exposition.