Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number

Dakai Guo; Ruichen Qiu; Ruyong Feng; Xiao-Shan Gao; Yichuan Cao

arxiv: 2606.26035 · v1 · pith:LSS4ENGEnew · submitted 2026-06-24 · 🧮 math.NT · cs.SC

Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number

Yichuan Cao , Dakai Guo , Ruichen Qiu , Ruyong Feng , Xiao-Shan Gao This is my paper

Pith reviewed 2026-06-25 19:24 UTC · model grok-4.3

classification 🧮 math.NT cs.SC

keywords triangular numberspentagonal numbersheptagonal numberspolygonal number sumsOEIS A287616number representations

0 comments

The pith

Any nonnegative integer equals a triangular number plus a pentagonal number plus a heptagonal number.

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

The paper establishes that every nonnegative integer n can be written as the sum of one triangular number, one pentagonal number, and one heptagonal number. This representation uses the standard formulas x(x+1)/2 for triangular, y(3y+1)/2 for pentagonal, and z(5z+1)/2 for heptagonal numbers, with x, y, z nonnegative integers. The result confirms a conjecture listed as OEIS A287616. The proof combines analytic arguments with computer verification and has been largely formalized in Lean 4.

Core claim

For every nonnegative integer n there exist nonnegative integers x, y, z satisfying n = x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2.

What carries the argument

The three-term representation of n using the closed formulas for the x-th triangular, y-th pentagonal, and z-th heptagonal numbers.

If this is right

The OEIS conjecture A287616 is settled.
Every nonnegative integer belongs to the set generated by adding one term from each of the three polygonal sequences.
The result supplies an explicit three-term polygonal sum covering all nonnegative integers.

Where Pith is reading between the lines

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

Similar covering statements may hold when one or more of the polygonal indices are replaced by other fixed polygons.
The explicit formulas make it feasible to compute the required x, y, z for any given n by bounded search.
The Lean formalization leaves only two external statements unchecked, so the computational part of the argument is already machine-verified.

Load-bearing premise

The symbolic computation check of one intermediate statement in the proof holds.

What would settle it

Exhibiting one nonnegative integer that cannot be written as such a sum.

read the original abstract

In this paper, it is proved that any nonnegative integer can be written in the following form $$ x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2, \qquad x,y,z \in \mathbb{N}. $$ This settles the conjecture recorded as OEIS A287616. All parts of the proof have been formalized in Lean 4, with the exception of two results: one externally cited theorem and one statement verified by symbolic computation. Both the natural-language proof and the Lean formalization were generated by the MechMath Agent Team developed by the authors.

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

The paper settles the OEIS conjecture with a Lean-formalized proof, aside from one symbolic step.

read the letter

Hi,

The main takeaway is that this paper proves every nonnegative integer is a sum of one triangular, one pentagonal, and one heptagonal number, which settles the open OEIS A287616 conjecture. They supply both a natural-language write-up and a Lean 4 formalization, generated by their MechMath agent.

The formalization is the part that stands out. It covers the bulk of the argument, leaving out only one externally cited theorem and one statement checked by symbolic computation. That level of machine verification is useful for a result like this, because it lets others confirm most of the case analysis and reductions without redoing the work by hand. The approach appears to be standard for these problems: reduce the representation to finitely many residue classes or small values, then handle the rest with known facts about the quadratic forms.

The result itself is new in the narrow sense that no prior proof existed for this exact triple. It does not reorganize broader additive number theory or introduce techniques that would apply to other polygonal sums.

The soft spot is exactly the one the abstract flags. The symbolic computation step sits outside the Lean code, so the completeness of the proof rests on that computation being correct. If it contains an error or misses a case, the representation theorem would have a gap. The AI generation of both the text and the formal code is also something a referee would want to examine, to confirm that the natural-language version matches the checked code and that no human oversight was skipped.

This paper is for readers who follow polygonal number sums or formal methods in number theory. It is too specific to interest most people outside those areas, but the conjecture resolution plus the partial formalization gives it a clear target audience.

I would send it to peer review. The combination of settling a recorded conjecture and providing substantial Lean coverage makes the details worth checking, especially the unformalized step.

Best,

Referee Report

1 major / 0 minor

Summary. The paper claims to prove that every nonnegative integer can be expressed as the sum of a triangular number, a pentagonal number, and a heptagonal number in the form x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2 for x,y,z nonnegative integers. This settles OEIS conjecture A287616. The argument is formalized in Lean 4 except for one externally cited theorem and one statement verified by symbolic computation; both the natural-language proof and the formalization were produced by the MechMath Agent Team.

Significance. If the result holds, the manuscript resolves an open conjecture in additive number theory. A notable strength is the machine-checked Lean 4 formalization covering most of the derivation, which supplies substantial verification and enhances the reliability of the central representation claim.

major comments (1)

[Abstract] Abstract: the proof is stated to be complete except for one statement verified only by symbolic computation (excluded from the Lean 4 formalization). This step is load-bearing for establishing the representation for all nonnegative integers; any gap or error in the computation would leave the theorem unproven in full.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation of minor revision. We address the single major comment below.

read point-by-point responses

Referee: [Abstract] Abstract: the proof is stated to be complete except for one statement verified only by symbolic computation (excluded from the Lean 4 formalization). This step is load-bearing for establishing the representation for all nonnegative integers; any gap or error in the computation would leave the theorem unproven in full.

Authors: We agree that the symbolic computation is load-bearing and that any error there would affect the full result. The manuscript already discloses this exception explicitly. To address the concern, the revised version will expand the abstract to specify the exact statement verified by symbolic computation, the computer algebra system(s) employed, and the finite range or conditions under which the check was performed, thereby making the verification status more transparent. revision: yes

Circularity Check

0 steps flagged

No circularity: direct formal derivation in Lean with external exceptions noted

full rationale

The paper proves the representation theorem via a Lean 4 formalization of the full argument chain, citing one external theorem and one symbolic computation result as the only unformalized parts. No steps reduce by definition, by fitted parameters renamed as predictions, or by self-citation chains that collapse the central claim to its own inputs. The derivation is self-contained as a machine-checked proof against the stated assumptions and does not invoke any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard arithmetic properties of natural numbers together with the definitions of the three polygonal numbers; the Lean formalization adds no new free parameters or invented entities.

axioms (1)

standard math Basic arithmetic properties of natural numbers and the definitions of triangular, pentagonal, and heptagonal numbers
The formalization in Lean relies on the standard mathematical library for these foundational definitions and properties.

pith-pipeline@v0.9.1-grok · 5647 in / 1179 out tokens · 48485 ms · 2026-06-25T19:24:05.556829+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

10 extracted references · 4 canonical work pages

[1]

J.W.S. Cassels. Rational quadratic forms. volume 74 ofNorth-Holland Mathematics Studies, pp. 9–
[2]

doi: https://doi.org/10.1016/S0304-0208(08)70410-9

North-Holland, 1982. doi: https://doi.org/10.1016/S0304-0208(08)70410-9. URLhttps://www. sciencedirect.com/science/article/pii/S0304020808704109

work page doi:10.1016/s0304-0208(08)70410-9 1982
[3]

Mechmath agent team

MechMath Team. Mechmath agent team. Academy of Mathematics and Systems Science, Chinese Academy of Sciences, 2026. URLhttps://mechmath.github.io

2026
[4]

The on-line encyclopedia of integer sequences, A287616

OEIS Foundation Inc. The on-line encyclopedia of integer sequences, A287616. Published electronically athttps://oeis.org/A287616, 2026

2026
[5]

Timothy O’Meara.Introduction to Quadratic Forms

O. Timothy O’Meara.Introduction to Quadratic Forms. Classics in Mathematics. Springer Berlin, Heidel- berg, 2000. ISBN 978-3-540-66564-9. doi: 10.1007/978-3-642-62031-7. Originally published as Volume 117 in the series: Grundlehren der mathematischen Wissenschaften

work page doi:10.1007/978-3-642-62031-7 2000
[6]

John Wiley & Sons, 1998

Alexander Schrijver.Theory of linear and integer programming. John Wiley & Sons, 1998

1998
[7]

Graduate Texts in Mathematics

Jean-Pierre Serre.A Course in Arithmetic. Graduate Texts in Mathematics. Springer New York, NY, 1973. ISBN 978-0-387-90040-7. doi: 10.1007/978-1-4684-9884-4. Original French edition with the title:Cours d’arithmetique

work page doi:10.1007/978-1-4684-9884-4 1973
[8]

Universal sums of three quadratic polynomials.Science China Mathematics, 63(3):501– 520, 3 2020

Zhi-Wei Sun. Universal sums of three quadratic polynomials.Science China Mathematics, 63(3):501– 520, 3 2020. ISSN 1869-1862. doi: 10.1007/s11425-017-9354-4. URLhttps://doi.org/10.1007/ s11425-017-9354-4

work page doi:10.1007/s11425-017-9354-4 2020
[9]

Arithmetic progressions represented by diagonal ternary quadratic forms, 2024

Hai-Liang Wu and Zhi-Wei Sun. Arithmetic progressions represented by diagonal ternary quadratic forms, 2024. URLhttps://arxiv.org/abs/1811.05855. 16 Key Laboratory of Mathematics Mechanization MechMath Agent Team A Determinacy certificate This appendix details the enumeration behind Lemma 11 and Remark 12. We first fix the vocabulary. A readis a single si...

arXiv 2024
[10]

These oddness checks are load-bearing because the good residue classes are modulo 6 and 10, not only modulo 3 and 5

In theP vw window row, the stronger congruencev≡w(mod 8), rather than merely modulo 4, makes (v+3w)/4 and(w−5v)/4 odd. These oddness checks are load-bearing because the good residue classes are modulo 6 and 10, not only modulo 3 and 5. C.4 Why the residual cone is the leftover Suppose a normalized primitive state is non-good. If it is not all odd, the sec...

[1] [1]

J.W.S. Cassels. Rational quadratic forms. volume 74 ofNorth-Holland Mathematics Studies, pp. 9–

[2] [2]

doi: https://doi.org/10.1016/S0304-0208(08)70410-9

North-Holland, 1982. doi: https://doi.org/10.1016/S0304-0208(08)70410-9. URLhttps://www. sciencedirect.com/science/article/pii/S0304020808704109

work page doi:10.1016/s0304-0208(08)70410-9 1982

[3] [3]

Mechmath agent team

MechMath Team. Mechmath agent team. Academy of Mathematics and Systems Science, Chinese Academy of Sciences, 2026. URLhttps://mechmath.github.io

2026

[4] [4]

The on-line encyclopedia of integer sequences, A287616

OEIS Foundation Inc. The on-line encyclopedia of integer sequences, A287616. Published electronically athttps://oeis.org/A287616, 2026

2026

[5] [5]

Timothy O’Meara.Introduction to Quadratic Forms

O. Timothy O’Meara.Introduction to Quadratic Forms. Classics in Mathematics. Springer Berlin, Heidel- berg, 2000. ISBN 978-3-540-66564-9. doi: 10.1007/978-3-642-62031-7. Originally published as Volume 117 in the series: Grundlehren der mathematischen Wissenschaften

work page doi:10.1007/978-3-642-62031-7 2000

[6] [6]

John Wiley & Sons, 1998

Alexander Schrijver.Theory of linear and integer programming. John Wiley & Sons, 1998

1998

[7] [7]

Graduate Texts in Mathematics

Jean-Pierre Serre.A Course in Arithmetic. Graduate Texts in Mathematics. Springer New York, NY, 1973. ISBN 978-0-387-90040-7. doi: 10.1007/978-1-4684-9884-4. Original French edition with the title:Cours d’arithmetique

work page doi:10.1007/978-1-4684-9884-4 1973

[8] [8]

Universal sums of three quadratic polynomials.Science China Mathematics, 63(3):501– 520, 3 2020

Zhi-Wei Sun. Universal sums of three quadratic polynomials.Science China Mathematics, 63(3):501– 520, 3 2020. ISSN 1869-1862. doi: 10.1007/s11425-017-9354-4. URLhttps://doi.org/10.1007/ s11425-017-9354-4

work page doi:10.1007/s11425-017-9354-4 2020

[9] [9]

Arithmetic progressions represented by diagonal ternary quadratic forms, 2024

Hai-Liang Wu and Zhi-Wei Sun. Arithmetic progressions represented by diagonal ternary quadratic forms, 2024. URLhttps://arxiv.org/abs/1811.05855. 16 Key Laboratory of Mathematics Mechanization MechMath Agent Team A Determinacy certificate This appendix details the enumeration behind Lemma 11 and Remark 12. We first fix the vocabulary. A readis a single si...

arXiv 2024

[10] [10]

These oddness checks are load-bearing because the good residue classes are modulo 6 and 10, not only modulo 3 and 5

In theP vw window row, the stronger congruencev≡w(mod 8), rather than merely modulo 4, makes (v+3w)/4 and(w−5v)/4 odd. These oddness checks are load-bearing because the good residue classes are modulo 6 and 10, not only modulo 3 and 5. C.4 Why the residual cone is the leftover Suppose a normalized primitive state is non-good. If it is not all odd, the sec...