What was already known
The authors of the original subsum-polynomial program posed ten conjectures and proved several reductions. The six statements here remained open.
AI involvement
AxiomProver produced the Lean statements and proofs from supplied conjectures without human script repairs. Chen, Ono and Zhang reconstructed the prose arguments and distinguished the corrected statements.
The model produced complete proofs for open supplied conjectures and found a counterexample, while the conjectures, earlier reductions and human exposition came from mathematicians.
Importance
Resolves six named conjectures and identifies a needed correction to another printed claim.
Limitations
Conjectures 5 and 7 are equivalent. The n>5 version of binary log-concavity remains open. The repository reports Lean 4.28.0 proofs and statement-comparator mappings; their match to the intended corrected statements is not independently established.
Technical verification
The six final claims have reported machine-checkable Lean 4.28.0 proofs and statement-comparator artifacts. The final files were not rebuilt here; careful reading of an earlier prose draft is not counted as complete human checking.
Formal checking
AxiomProver-generated Lean proofs and comparator mappings to supplied statements
- Checker
- Lean 4 kernel and comparator artifacts in AxiomMath/PartitionPolynomial
- Scope
- Conjectures 2, 5, 7, 8, 9 and corrected 10 as formalized for the paper
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The authors give human explanations of the cyclotomic noncancellation, partition specializations and ternary recurrence in Sections 3–6.
Correction and publication history
Resolves six named conjectures and identifies a needed correction to another printed claim.
Read this published revision