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

In this paper, it is proved that any nonnegative integer can be written in the following form $$x(x+1)\mathrm{/}2+y(3y+1)\mathrm{/}2+z(5z+1)\mathrm{/}2,x,y,z\in \mathbb{N}\mathrm{.}$$ 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.