Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number
2026-06-24 • Symbolic Computation
Symbolic Computation
AI summaryⓘ
The authors proved that any whole number can be written as a sum of three special formulas involving three numbers x, y, and z. These formulas are based on simple arithmetic sequences called polygonal numbers. Their proof fully answers a previously known math puzzle from an online database. They also created a computer-verified version of their proof, except for two parts: one taken from another source and one checked by a computer program. The authors used an automated system called the MechMath Agent Team to help write both the explanation and the computer proof.
nonnegative integerpolygonal numberstriangular numberformal proofLean 4symbolic computationOEISautomated theorem proving
Authors
Yichuan Cao, Dakai Guo, Ruichen Qiu, Ruyong Feng, Xiao-Shan Gao
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.