Binary subsum-polynomial coprimality

For a partition λ of n, its subsum polynomial is sp(λ,x)=∏ᵢ(1+x^λᵢ). Sum 1/sp over the specified partition family, combine over the denominator ∏ⱼ(1+xʲ)^⌊n/j⌋ for allowed parts j, then cancel the greatest common factor of the individual numerator summands.

For binary partitions, whose parts are powers of two, are the resulting numerator num_B(n,x) and denominator den_B(n,x) coprime in Z[x] for every n≥1?

Why it matters and what counts as progress

Why it matters: Coprimality asks whether the prescribed common-summand cancellation already leaves the reciprocal sum in lowest terms.

What counts as progress: A proof excluding all remaining possible cyclotomic factors for every n, or a binary numerator and denominator sharing a nonconstant factor.

How the problem developed

11 May 2026 · Conjecture [1]
Cristina Ballantine, George Beck, Brooke Feigon and Kathrin Maurischat Introduced binary subsum polynomials and conjectured that the reduced numerator and denominator are relatively prime for every n.
20 May 2026 · Reported claim [2]
Evan Chen, Ken Ono and Jujian Zhang Proved binary numerator-denominator coprimality for every n by ruling out the possible cyclotomic factors.

AI contribution

Reciprocals of Partition Polynomials

Evan Chen, Ken Ono, Jujian Zhang

AxiomProver generated Lean proofs of Ballantine–Beck–Feigon–Maurischat Conjectures 2, 5, 7, 8, 9 and the intended corrected reading of 10, covering coprimality, divisibility, special values and a recurrence. It also found an n=4 counterexample to a printed binary log-concavity claim.

AI involvementAI-centered

ImportanceNotable

Technical verificationFormal (Lean 4.28.0 with mathlib and comparator)

Human understandingFull