Reciprocals of Partition Polynomials

Ballantine–Beck–Feigon–Maurischat introduced the subsum polynomial $$\mathrm{sp}(\lambda ,x):=\prod _i(1+x^{{\lambda }_i})$$ attached to an integer partition $\lambda$, and studied rational functions obtained by summing reciprocals of these polynomials over natural classes of partitions. They posed ten conjectures which naturally divide into coprimality and divisibility questions, special-value and recurrence formulas, and coefficient-shape problems. We prove all of the conjectures in the first two families: the ordinary and binary coprimality/divisibility conjectures, and the odd and ternary special-value/recurrence conjectures. AxiomProver autonomously produced Lean/mathlib formalizations and machine-checkable proofs of these six conjectures, and also discovered a counterexample to the statement as printed; the corrected form remains open.