Ballantine, Beck, Feigon, and Maurischat introduced subsum polynomials attached to integer partitions and posed ten conjectures about rational functions formed by summing reciprocals of these polynomials over natural classes of partitions. The conjectures concern coprimality/divisibility and special-value/recurrence properties.

The authors prove six of the ten conjectures spanning two families: the ordinary and binary coprimality/divisibility conjectures, and the odd and ternary special-value/recurrence conjectures. The proofs use cyclotomic polynomial techniques, analyzing which roots of unity annihilate the reduced numerator polynomial by tracking how cyclotomic factors distribute across partition summands. AxiomProver autonomously produced Lean/mathlib formalizations and machine-checkable proofs of these six conjectures, and also discovered a counterexample to one conjecture as printed.

All six conjectures in the coprimality/divisibility and special-value/recurrence families are proved. A counterexample to one conjecture as originally stated was found by the automated prover; the corrected form remains open.