Reciprocals of Partition Polynomials

TL;DR

This paper proves several conjectures related to reciprocals of partition polynomials, specifically addressing coprimality, divisibility, and special-value properties, with formal proofs verified by automated tools.

Contribution

It confirms six conjectures in the area of reciprocals of partition polynomials and identifies a false conjecture through formalized proof and counterexample.

Findings

Proved all conjectures in coprimality and special-value families.

Discovered a counterexample to the binary log-concavity conjecture.

Formalized proofs using Lean/mathlib and automated theorem proving.

Abstract

Ballantine--Beck--Feigon--Maurischat introduced the subsum polynomial \[ \operatorname{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 olynomials 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 the counterexample showing that the binary log-concavity conjecture is false as stated.