Reciprocals of Partition Polynomials

Evan Chen; Jujian Zhang; Ken Ono

arxiv: 2605.21718 · v2 · pith:RKPOMQGSnew · submitted 2026-05-20 · 🧮 math.CO

Reciprocals of Partition Polynomials

Evan Chen , Ken Ono , Jujian Zhang This is my paper

Pith reviewed 2026-05-25 05:58 UTC · model grok-4.3

classification 🧮 math.CO

keywords partition polynomialssubsum polynomialscoprimality conjecturesdivisibilityrecurrence formulasspecial valuesformal verificationinteger partitions

0 comments

The pith

Six conjectures on sums of reciprocals of subsum polynomials are proved via formalization.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper examines rational functions formed by summing the reciprocals of subsum polynomials attached to integer partitions. Earlier work posed ten conjectures about coprimality, divisibility, special values, and recurrences for these sums over natural classes of partitions. The authors establish all six conjectures belonging to the ordinary and binary coprimality/divisibility families and the odd and ternary special-value/recurrence families. Autonomous production of Lean formalizations supplies machine-checkable proofs of these statements. One conjecture statement as originally printed is shown to be incorrect, though the corrected version is proved.

Core claim

We prove the ordinary and binary coprimality/divisibility conjectures and the odd and ternary special-value/recurrence conjectures for the rational functions obtained by summing reciprocals of subsum polynomials over appropriate classes of partitions. These proofs were obtained through machine-generated Lean formalizations.

What carries the argument

The subsum polynomial sp(λ, x) defined as the product over i of (1 + x to the power λ_i), together with the sums of the reciprocals of these polynomials over classes of partitions.

If this is right

The ordinary sums of reciprocals are coprime to given integers in the manner stated by the conjectures.
The binary versions of the sums satisfy the corresponding divisibility relations.
The odd cases of the sums take on explicit special values at the points considered.
The ternary cases obey the stated recurrence relations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The autonomous formalization technique could be applied directly to the four remaining coefficient-shape conjectures.
Similar machine-generated proofs might resolve related open questions about generating functions for partitions.
The identification of the printed error indicates that formalization can serve as an independent check on conjecture statements before they are accepted.

Load-bearing premise

The Lean formalizations produced by AxiomProver correctly encode the mathematical statements of the six conjectures after correction of the one printed statement.

What would settle it

An explicit small partition for which the sum of reciprocals violates one of the six proved coprimality, divisibility, special-value or recurrence properties.

read the original abstract

Ballantine--Beck--Feigon--Maurischat introduced the subsum polynomial \[ \operatorname{sp}(\lambda,x):=\prod_i (1+x^{\lambda_i}) \] attached to an integer partition $\lambda$, and studied rational functions obtained by summing reciprocals of these polynomials over natural classes of partitions. They posed ten conjectures which naturally divide into coprimality and divisibility questions, special-value and recurrence formulas, and coefficient-shape problems. We prove all of the conjectures in the first two families: the ordinary and binary coprimality/divisibility conjectures, and the odd and ternary special-value/recurrence conjectures. AxiomProver autonomously produced Lean/mathlib formalizations and machine-checkable proofs of these six conjectures, and also discovered a counterexample to the statement as printed; the corrected form remains open.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Lean formalizations settle six open conjectures on partition polynomial reciprocals and flag one printed error.

read the letter

The main point is that this paper closes six of the ten conjectures from Ballantine-Beck-Feigon-Maurischat on sums of reciprocals of subsum polynomials. The authors deliver machine-checked Lean proofs for the ordinary and binary coprimality/divisibility claims plus the odd and ternary special-value/recurrence ones, and the formalization process found a counterexample to the statement as originally printed. The corrected version stays open. That is the concrete advance: new, reproducible proofs for previously unresolved statements, backed by mathlib rather than hand derivation alone. The formal step adds value here because these are exact arithmetic claims that can be encoded and checked independently. The paper does a clean job of stating what was conjectured, what is now verified, and what remains. The soft spots are proportionate. Only the first two families are addressed, so the coefficient-shape problems are untouched. The work is narrow by design and does not claim broader impact. Without the full manuscript it is hard to judge how much the Lean statements match the originals beyond the tool's output, but the fact that it caught the printed error is evidence the process is functioning. This is for people already working on partition polynomials or on formal verification in combinatorics. A reader tracking those specific conjectures gets direct utility from the resolved cases and the correction. It is not a wide-audience paper, but the evidence is solid enough that it deserves a serious referee. The formal results are new content on open questions, so peer review makes sense even if the remaining conjectures and presentation details need work.

Referee Report

1 major / 0 minor

Summary. The manuscript claims to prove the six conjectures in the first two families (ordinary and binary coprimality/divisibility; odd and ternary special-value/recurrence) on reciprocals of subsum polynomials sp(λ,x) introduced by Ballantine--Beck--Feigon--Maurischat. Proofs are supplied by AxiomProver-generated Lean/mathlib formalizations that are machine-checkable; the work also reports discovering a counterexample to one statement as printed in the source paper, with the corrected form noted as remaining open.

Significance. If the Lean encodings correctly capture the original mathematical statements, the machine-checked proofs supply independent, reproducible verification of the six conjectures. The fact that the same formalization process located a counterexample to a printed claim further supports the reliability of the method and strengthens the contribution to the study of partition polynomials.

major comments (1)

[Abstract] Abstract: the claim that 'we prove all of the conjectures in the first two families' (i.e., all six) is in tension with the subsequent statement that 'the corrected form remains open.' The main text must explicitly identify which of the six statements have been formally verified and the precise status of the corrected conjecture.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and for identifying the need for greater clarity in the abstract and main text. We will revise the manuscript accordingly to explicitly distinguish the six verified conjectures from the separate corrected statement that remains open.

read point-by-point responses

Referee: [Abstract] Abstract: the claim that 'we prove all of the conjectures in the first two families' (i.e., all six) is in tension with the subsequent statement that 'the corrected form remains open.' The main text must explicitly identify which of the six statements have been formally verified and the precise status of the corrected conjecture.

Authors: The six conjectures in the first two families (ordinary and binary coprimality/divisibility; odd and ternary special-value/recurrence) are the ones that have been formally verified by the AxiomProver-generated Lean/mathlib proofs. The counterexample and corrected form that remains open refers to a different statement appearing in the source paper of Ballantine--Beck--Feigon--Maurischat, not to any of these six conjectures. We will revise both the abstract and the relevant sections of the main text to state this distinction explicitly, listing the verified conjectures and clarifying the status of the separate corrected conjecture. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's central claims consist of proofs of six conjectures originally posed by Ballantine--Beck--Feigon--Maurischat (distinct authors). These proofs are supplied by autonomous Lean/mathlib formalizations generated by the external AxiomProver tool, with one printed statement corrected after counterexample discovery. No load-bearing steps reduce to self-definitions, fitted parameters renamed as predictions, or self-citation chains; the verification is performed against the independent mathlib library and is machine-checkable. This satisfies the criterion of self-contained results against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claims rest on standard mathematical axioms of combinatorics and the correctness of the Lean encoding of the conjectures; no free parameters, ad-hoc entities, or fitted constants appear in the abstract description.

axioms (1)

standard math Standard axioms of integer partitions and polynomial rings over the integers
Invoked implicitly when defining subsum polynomials and their reciprocal sums.

pith-pipeline@v0.9.0 · 5662 in / 1153 out tokens · 33104 ms · 2026-05-25T05:58:28.439574+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We prove all of the conjectures in the first two families: the ordinary and binary coprimality/divisibility conjectures, and the odd and ternary special-value/recurrence conjectures.
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

num(n,ζ_{2d}) = C_{n,d} num(r,ζ_{2d}) … all surviving summands lie on a single open ray

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

4 extracted references · 4 canonical work pages · 1 internal anchor

[1]

G. E. Andrews,The Theory of Partitions, Encyclopedia of Mathematics and Its Applications, Vol. 2, Addison- Wesley, Reading, MA, 1976

work page 1976
[2]

Reciprocals of Subsum Polynomials

C. Ballantine, G. Beck, B. Feigon, and K. Maurischat,Reciprocals of subsum polynomials, arXiv:2605.10512, posted May 11, 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026
[3]

ThemathlibCommunity, TheLeanmathematicallibrary, inProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020

work page 2020
[4]

de Moura, S

L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer, The Lean theorem prover (system description), inAutomated Deduction – CADE-25, Lecture Notes in Computer Science 9195, Springer, 2015, 378–388. Axiom Math, 124 University A venue, Palo Alto, CA 94301 Email address:evan@axiommath.ai Email address:ken@axiommath.ai Email address:jujian@axiommath.ai

work page 2015

[1] [1]

G. E. Andrews,The Theory of Partitions, Encyclopedia of Mathematics and Its Applications, Vol. 2, Addison- Wesley, Reading, MA, 1976

work page 1976

[2] [2]

Reciprocals of Subsum Polynomials

C. Ballantine, G. Beck, B. Feigon, and K. Maurischat,Reciprocals of subsum polynomials, arXiv:2605.10512, posted May 11, 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026

[3] [3]

ThemathlibCommunity, TheLeanmathematicallibrary, inProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020

work page 2020

[4] [4]

de Moura, S

L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer, The Lean theorem prover (system description), inAutomated Deduction – CADE-25, Lecture Notes in Computer Science 9195, Springer, 2015, 378–388. Axiom Math, 124 University A venue, Palo Alto, CA 94301 Email address:evan@axiommath.ai Email address:ken@axiommath.ai Email address:jujian@axiommath.ai

work page 2015