Odd-partition numerator at minus one

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 partitions into odd parts, does num_O(n,−1) equal the largest odd divisor of n! for every n≥1?

Why it matters and what counts as progress

Why it matters: The special value would identify an exact factorial arithmetic structure in a rational partition sum.

What counts as progress: An all-n evaluation formula or an explicit n where it fails, using the common-summand cancellation convention for num_O.

How the problem developed

11 May 2026 · Definition and conjectures [1]
Cristina Ballantine, George Beck, Brooke Feigon and Kathrin Maurischat Introduced subsum polynomials and conjectured arithmetic properties of their reciprocal sums, including special-value questions for odd partitions.
20 May 2026 · Theorem [2]
Evan Chen, Ken Ono and Jujian Zhang; AxiomProver Proved the odd-partition special-value conjecture: the numerator at −1 is the largest odd divisor of n! for every n≥1. The paper reports autonomous Lean proofs.

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