Sum of a triangular number, a generalized pentagonal number, and a generalized heptagonal number

Any nonnegative integer can be written as $x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2$ with $x, y, z$ nonnegative integers.

Zhi-Wei Sun has offered a USD 135 prize for the first proof of this conjecture.

References:

• OEIS A287616
• Zhi-Wei Sun, "Universal sums of three quadratic polynomials", arXiv:1502.03056 [math.NT]

def OeisA287616.IsSumOfTriangularAndGeneralizedPolygonal (n : ℕ) : Prop

The predicate that n can be written as $x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2$ for nonnegative integers $x, y, z$.

Equations

• OeisA287616.IsSumOfTriangularAndGeneralizedPolygonal n = ∃ (x : ℕ) (y : ℕ) (z : ℕ), n = x * (x + 1) / 2 + y * (3 * y + 1) / 2 + z * (5 * z + 1) / 2

theorem OeisA287616.isSumOfTriangularAndGeneralizedPolygonal_0 : IsSumOfTriangularAndGeneralizedPolygonal 0

theorem OeisA287616.isSumOfTriangularAndGeneralizedPolygonal_1 : IsSumOfTriangularAndGeneralizedPolygonal 1

theorem OeisA287616.isSumOfTriangularAndGeneralizedPolygonal_2 : IsSumOfTriangularAndGeneralizedPolygonal 2

theorem OeisA287616.isSumOfTriangularAndGeneralizedPolygonal_4 : IsSumOfTriangularAndGeneralizedPolygonal 4

theorem OeisA287616.conjecture (n : ℕ) : IsSumOfTriangularAndGeneralizedPolygonal n

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.