Sum of two squares, a power of 3, and a power of 5

Any integer $n > 1$ can be written as $a^2 + b^2 + 3^c + 5^d$ where $a, b, c, d$ are nonnegative integers.

Zhi-Wei Sun has offered a $3,500 prize for the first proof.

References:

• OEIS A303656
• Z.-W. Sun, "Restricted sums of four squares," arXiv preprint: https://arxiv.org/abs/1701.05868v10
• Z.-W. Sun, "Refining Lagrange's four-square theorem," Journal of Number Theory: http://maths.nju.edu.cn/~zwsun/RefineFourSquareTh.pdf
• Z.-W. Sun, "Restricted sums of three or four squares": http://maths.nju.edu.cn/~zwsun/Square-sum.pdf
• Zhi-Wei Sun's 1-3-5 conjecture and variations: https://www.aimspress.com/aimspress-data/era/2020/2/PDF/1935-9179_2020_2_589.pdf

def OeisA303656.IsSumOfTwoSquaresAndPowersOf3And5 (n : ℕ) : Prop

The predicate that n can be written as $a^2 + b^2 + 3^c + 5^d$ for nonnegative integers.

Equations

• OeisA303656.IsSumOfTwoSquaresAndPowersOf3And5 n = ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ), n = a ^ 2 + b ^ 2 + 3 ^ c + 5 ^ d

theorem OeisA303656.isSumOfTwoSquaresAndPowersOf3And5_2 : IsSumOfTwoSquaresAndPowersOf3And5 2

theorem OeisA303656.isSumOfTwoSquaresAndPowersOf3And5_5 : IsSumOfTwoSquaresAndPowersOf3And5 5

theorem OeisA303656.isSumOfTwoSquaresAndPowersOf3And5_25 : IsSumOfTwoSquaresAndPowersOf3And5 25

theorem OeisA303656.conjecture (n : ℕ) (hn : 1 < n) : IsSumOfTwoSquaresAndPowersOf3And5 n

Zhi-Wei Sun's Conjecture (A303656): Any integer $n > 1$ can be written as the sum of two squares, a power of 3, and a power of 5.