Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number
Settles a specific number theory conjecture (OEIS A287616) for mathematicians interested in polygonal number representations.
The paper proves that every nonnegative integer can be expressed as a sum of a triangular, a pentagonal, and a heptagonal number, settling a known conjecture. The proof is formalized in Lean 4, with the natural-language proof and formalization generated by an AI agent team.
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.