Ternary-partition numerator recurrence

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.

Set t(n)=num_T(n,1) for ternary partitions and t(0)=1. The intended recurrence is t(3n)=t(3n+1)=t(3n+2) for n≥0 and t(3n)−t(3n−2)=2^(2n)t(n) for n≥1.

Why it matters and what counts as progress

Why it matters: A recurrence compresses the entire special-value sequence, while the placement of the difference operator changes the mathematical claim.

What counts as progress: A proof of the stated corrected recurrence with its initial convention, or a counterexample; applying the difference after division is the false literal printed reading.

How the problem developed

11 May 2026 · Conjecture [1]
Cristina Ballantine, George Beck, Brooke Feigon, and Kathrin Maurischat Introduced reciprocal subsum polynomials and stated special-value and recurrence conjectures for odd and ternary partition families.
20 May 2026 · Recurrence [2]
Evan Chen, Ken Ono, and Jujian Zhang, with AxiomProver-generated Lean proofs Proved the ternary numerator recurrence among six formalized results resolving conjectures from the subsum-polynomial program.

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