🔢 mathematics

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

This paper proves that every nonnegative integer can be expressed as the sum of a triangular, a pentagonal, and a heptagonal number, thereby settling the OEIS A287616 conjecture using a proof generated by the MechMath Agent Team and formalized in Lean 4.

Original authors: Yichuan Cao, Dakai Guo, Ruichen Qiu, Ruyong Feng, Xiao-Shan Gao

Published 2026-06-25

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Yichuan Cao, Dakai Guo, Ruichen Qiu, Ruyong Feng, Xiao-Shan Gao

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you have a giant, infinite bag of numbers: 0, 1, 2, 3, and so on forever. Mathematicians have long wondered if every single one of these numbers can be built by stacking three specific types of "shape blocks" on top of each other.

This paper, written by a team of AI agents called the MechMath Agent Team, says: Yes, you can.

Here is the simple breakdown of what they did, using everyday analogies.

The Three Magic Blocks

The authors are trying to build any number $n$ using a specific recipe:
$n = \text{Triangular Block} + \text{Pentagonal Block} + \text{Heptagonal Block}$

Triangular Blocks: Think of stacking coins in a triangle (1, 3, 6, 10...).
Pentagonal Blocks: Think of stacking coins in a pentagon shape (1, 5, 12, 22...).
Heptagonal Blocks: Think of stacking coins in a seven-sided shape (1, 7, 18, 34...).

The question was: Can you make every number (like 1, 100, or 1,000,000) by picking one of each of these blocks and adding them together? This was a guess (conjecture) recorded in a famous math database (OEIS A287616).

The Transformation: Turning Shapes into Squares

To solve this, the team didn't try to stack the shapes directly. Instead, they used a mathematical "magic trick" (called a square reduction).

Imagine you have a wobbly, irregular puzzle piece. It's hard to fit. But if you cut it and rearrange it, it suddenly becomes a perfect square.

They took the messy triangular, pentagonal, and heptagonal formulas.
They rearranged them into a neat equation involving squares (like $15u^2 + 5v^2 + 3w^2$ ).
Now, instead of stacking shapes, the problem became: "Can we find three specific numbers ( $u, v, w$ ) that fit into this square equation to equal our target number?"

The Two-Step Strategy

The proof works like a two-step rescue mission to get the numbers into the right shape.

Step 1: The "Seed" (Finding a Starting Point)

First, they had to prove that a solution exists somewhere, even if it's in a weird, messy form.

The Analogy: Imagine you are lost in a forest. You know there is a path out, but you can't see it. The "Seed" is like finding a single, solid tree that proves you are definitely in the right forest.
They used advanced number theory (specifically "genus theory," which is like checking the DNA of the numbers) to prove that for any target number, there is at least one set of $u, v, w$ that works. This is the "unconditional primitive seed."

Step 2: The "Descent" (Walking Down the Mountain)

Finding a solution isn't enough; it has to be a good solution (where the numbers are positive and follow specific rules).

The Analogy: Imagine you are on a mountain peak (a messy solution). You need to get down to the valley floor (the perfect solution).
The team invented a set of "elevator buttons" (called moves). Each button transforms your current numbers into new numbers.
They defined a "potential score" (like an altitude meter). Every time you press a button, the score goes down.
The Problem: Most of the time, the buttons work perfectly. But there is a tiny, tricky "canyon" (the residual cone) where the buttons get stuck or behave strangely.
The Solution: For this tricky canyon, they didn't guess. They used a computer to map out every single possible path through the canyon. They proved that no matter where you start in the canyon, there is a short, specific sequence of button presses that will get you out.

The Role of the Computer (The "MechMath" Team)

This is where it gets cool. The authors didn't just write the proof; they built an AI agent team to write it for them.

The Human Part: They set up the rules and the logic.
The AI Part: The "MechMath Agent Team" generated the natural language explanation and the formal code.
The Verification: They used a digital proof-checker (Lean 4) to verify every single step. It's like having a super-strict librarian who checks every sentence of a book to make sure the logic holds up.
- The computer checked the "elevator buttons" and the "mountain descent."
- The only things the computer didn't check from scratch were two very famous, classical math theorems (which are like established laws of physics) and the final map of the tricky canyon (which was generated by a precise computer calculation).

The Conclusion

The paper proves that every non-negative integer can indeed be built from one triangular, one pentagonal, and one heptagonal number.

The Result: The guess was right.
The Method: They turned a shape problem into a square problem, found a starting point, and then proved you can always "walk down" to the perfect solution using a mix of clever math and a computer-generated map of the tricky parts.
The Legacy: The entire proof is now "machine-checked," meaning a computer has verified that the logic is unbreakable.

In short: They solved a 2,000-year-old style of puzzle by turning it into a square, finding a starting point, and using a computer to map the last few difficult steps, all while an AI team wrote the story and the code.

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

Problem Statement
The paper addresses a conjecture recorded as OEIS A287616, originally proposed by Zhi-Wei Sun. The conjecture posits that every nonnegative integer $n$ can be represented as the sum of a triangular number, a second pentagonal number, and a second heptagonal number. Formally, for every $n \in \mathbb{N}$ , there exist $x, y, z \in \mathbb{N}$ such that:
$n = \frac{x(x+1)}{2} + \frac{y(3y+1)}{2} + \frac{z(5z+1)}{2}$
The authors distinguish this from "generalized" polygonal number problems where variables may range over all integers; here, the variables are strictly nonnegative.

Methodology and Proof Strategy
The proof proceeds by transforming the additive problem into a constrained representation problem for a diagonal ternary quadratic form.

Square Reduction:
Using elementary identities ( $8T(x)+1=(2x+1)^2$ , etc.), the problem is reduced to representing integers of the form $m = 120n + 23$ by the quadratic form:
$Q(u, v, w) = 15u^2 + 5v^2 + 3w^2$
The goal becomes finding a representation where $u$ is positive and odd, $v \equiv 1 \pmod 6$ , and $w \equiv 1 \pmod{10}$ .
The Primitive Seed (Existence):
The proof first establishes that every $m \equiv 23 \pmod{120}$ admits a primitive integral representation by $Q$ (where $\gcd(u,v,w)=1$ ).
- Local-Global Principle: The authors utilize the Hasse–Minkowski theorem and the specific genus structure of $Q$ . The genus of $Q$ consists of exactly two classes: the class of $Q$ itself and the class of a "mate" form $g_2(x,y,z) = 2x^2 - 2xy + 8y^2 + 15z^2$ .
- Transfer: If $m$ is represented by the mate $g_2$ , a series of explicit transformations (involving involutions and rational isometries) transfers this representation to $Q$ , preserving primitivity. This step relies on classical number theory results (Hasse–Minkowski, genus theory) which are cited but not re-proven within the formalization.
Finite Descent (Convergence):
Once a primitive representation is secured, the proof employs a descent algorithm to reach a "good" state (satisfying the specific congruence conditions).
- Potential Function: A lexicographic potential $\Phi(u,v,w)$ is defined based on the parity and congruence status of the coordinates.
- Move Calculus: Three integer matrices ( $P_{uv}, P_{uw}, P_{vw}$ ) define "moves" that preserve the value of $Q$ and the primitivity of the representation while strictly lowering $\Phi$ .
- Elementary Descents: For most states, a single move suffices to improve the potential.
- Residual Cone: A small subset of states (the "residual cone") resists elementary descent. For these, the authors employ a finite-key determinacy argument. They prove that the success of any short sequence of moves depends only on a finite set of signs and residues (a "key") of the starting vector.
- Computer-Assisted Cover: The residual cone is covered by a finite set of "sign cones." For each cone, an exact rational linear programming (LP) certificate verifies that an escape word (a sequence of moves) exists. This verification is performed using exact integer and rational arithmetic, avoiding floating-point approximations.

Key Contributions and Results

Proof of Conjecture A287616: The paper provides a complete proof that the triple $(T, P, H)$ is universal for nonnegative integers.
Formalization in Lean 4: A significant portion of the mathematical core (Sections 2–5 and the descent logic) has been formalized in Lean 4 over the Mathlib library.
- The formalization includes the square reduction, the transport laws, the elementary descents, and the termination argument.
- The conjecture itself is machine-checked.
- The only exceptions to full formalization are:
  1. The classical genus local–global principle (Hasse–Minkowski + two-class genus fact), which is cited as an axiom.
  2. The finite cover of the residual cone, which is treated as a computer-verified input (an axiom derived from exact certificates).
MechMath Agent Team: The natural-language proof and the Lean formalization were generated by the authors' "MechMath Agent Team," demonstrating the capability of AI agents to produce rigorous, machine-verifiable mathematical proofs.

Significance and Claims
The paper claims to settle the OEIS A287616 conjecture through a combination of classical number theory and rigorous computer-assisted verification. Its significance lies in:

Rigorous Verification: By formalizing the proof in Lean, the authors ensure that the logical structure, the descent mechanics, and the equivalence transformations are free of human error.
Hybrid Proof Method: The work exemplifies a "hybrid" approach where deep theoretical results (genus theory) are combined with exhaustive, exact computer verification (linear programming covers) to solve a problem that is intractable by purely manual or purely heuristic means.
Transparency of Dependencies: The formalization explicitly isolates the non-formalized inputs (the cited classical theorems and the computer certificates), making the dependency structure of the proof auditable. The authors emphasize that the "mathematical core" is fully formalized, while the "computational input" is reduced to a finite, exact certificate.

The paper does not propose new applications or future experimental directions but focuses strictly on the resolution of the specific number-theoretic conjecture and the demonstration of the formalization pipeline.