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 $$x(x+1)/2+y(3y+1)/2+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.

23 pages