← All papers
Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number
math.NT
Jun 24, 2026 · v1
cs.SC
TL;DR
Formalizes in Lean 4 the proof that every nonnegative integer is a sum of a triangular, pentagonal, and 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, \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.
Problem
The conjecture (OEIS A287616) that every nonnegative integer can be written as x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2 remained open.
Approach
The proof proceeds by case analysis and arithmetic bounds. Both the natural-language proof and the Lean 4 formalization were generated by the MechMath Agent Team, with two exceptions: one externally cited theorem and one symbolic-computation step.
Results
The conjecture is settled affirmatively. All other parts of the proof are formalized in Lean 4.