Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number
Abstract
In this paper, it is proved that any nonnegative integer can be written in the following form $\frac{x(x+1)}2+\frac{y(3y+1)}2+\frac{z(5z+1)}2,\, 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.
