Paper Detail

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

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

arxiv Score 5.2

Published 2026-06-24 · First seen 2026-06-25

General AI

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.

Workflow Status

Review status
pending
Role
unreviewed
Read priority
later
Vote
Not set.
Saved
no
Collections
Not filed yet.
Next action
Not filled yet.

Reading Brief

No structured notes yet. Add `summary_sections`, `why_relevant`, `claim_impact`, or `next_action` in `papers.jsonl` to enrich this view.

Why It Surfaced

No ranking explanation is available yet.

Tags

No tags.

BibTeX

@article{cao2026every,
  title = {Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number},
  author = {Yichuan Cao and Dakai Guo and Ruichen Qiu and Ruyong Feng and Xiao-Shan Gao},
  year = {2026},
  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, \textbackslash{}qquad x,y,z \textbackslash{}in \textbackslash{}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 b},
  url = {https://arxiv.org/abs/2606.26035},
  keywords = {math.NT, cs.SC},
  eprint = {2606.26035},
  archiveprefix = {arXiv},
}

Metadata

{}