Formal target: Corpus.OEIS287616.conjecture
**Zhi-Wei Sun's Conjecture (A287616)**: Any nonnegative integer can be written as the sum of a triangular number $x(x+1)/2$, a generalized pentagonal number $y(3y+1)/2$, and a generalized heptagonal number $z(5z+1)/2$, where $x, y, z$ are nonnegative integers.
Exact formal statement
∀ (n : Nat), Corpus.OEIS287616.A nThis target is a formal statement, not a proof of the problem.
Environment availability: available.