Binary subsum-polynomial log-concavity

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, is the coefficient sequence of num_B(n,x) log-concave? The printed n≥2 claim fails at n=4; the intended corrected log-concavity range excludes n=4,5.

Why it matters and what counts as progress

Why it matters: Coefficient-shape constraints are separate from coprimality and special-value identities for these reciprocal sums.

What counts as progress: A proof or counterexample for the corrected n>5 range, or a precisely distinguished unimodality theorem; the n=4 counterexample refutes only the broader printed claim.

How the problem developed

11 May 2026 · Conjecture [1]
Cristina Ballantine, George Beck, Brooke Feigon and Kathrin Maurischat The original paper asserted log-concavity of the binary numerator for n≥2.
20 May 2026 · Counterexample [2]
Evan Chen, Ken Ono and Jujian Zhang Displayed the n=4 numerator, whose coefficient sequence is not log-concave; the corrected n>5 conjecture remains open.

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