Ordinary 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.

When the sum ranges over all ordinary partitions, are num(n,x) and den(n,x) coprime in Z[x] for every n≥1? Cancellation of the summands’ common factor does not make this automatic.

Why it matters and what counts as progress

Why it matters: The result determines whether additional cancellation can occur only after the numerator terms are added.

What counts as progress: A proof of numerator nonvanishing at every possible denominator root of unity, or a remaining common polynomial factor for some n.

How the problem developed

12 May 2026 · Conjecture [1]
Cristina Ballantine, George Beck, Brooke Feigon and Kathrin Maurischat Introduced subsum polynomials and posed ten conjectures about reciprocal sums; ordinary coprimality was among the open statements.
20 May 2026 · Partial result [2]
Evan Chen, Ken Ono and Jujian Zhang Proved the ordinary numerator-denominator coprimality conjecture for every n≥1 as one of six results on the conjecture list.
22 May 2026 · Formalization [3]
AxiomProver Reported Lean formalization of the ordinary coprimality result alongside five other conjecture results; the release also records a counterexample to a separate printed log-concavity claim.

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