The Ballantine-Beck-Feigon-Maurischat Conjectures on Subsum Polynomials
Ballantine, Beck, Feigon and Maurischat introduced the subsum polynomial attached to an integer partition , studied rational functions built by summing reciprocals of these polynomials over natural classes of partitions, and posed ten conjectures. Six are now proved: the ordinary and binary coprimality and divisibility conjectures, and the odd and ternary special-value and recurrence conjectures.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Partitions and q-series
- Posed by
- Ballantine, Beck, Feigon and Maurischat
- Year posed
- —
- Years open
- —
- Solved
- 2026-05-20
- Model
- AxiomProver
- Vendor
- —
- Collaborators
- Evan Chen, Ken Ono, Jujian Zhang
- Verification
- Lean-verified
- Publication
- Preprint
- Significance
- 25 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
six of the ten conjectures proved; one was found false as printed and its corrected form remains open
What the AI did
AxiomProver autonomously produced Lean and mathlib formalizations and machine-checkable proofs of all six conjectures. It also discovered a counterexample to one of the conjectures as printed, so the same system both proved and refuted statements drawn from one list, which is a useful demonstration that it was reading the statements rather than pattern-matching toward the expected answer.
Verification
The six proofs are Lean and mathlib formalizations, so they are machine-checkable rather than dependent on refereeing. Note that the catalog has not compiled the artifact itself, so this records the authors' claim of formalization, not an independent build.