Four-square conjecture with powers of 2, 3, and 5

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

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

References:

• OEIS A308734
• Z.-W. Sun, "Refining Lagrange's four-square theorem," J. Number Theory 175 (2017), 167-190. https://doi.org/10.1016/j.jnt.2016.11.008
• Z.-W. Sun, "Restricted sums of four squares," Int. J. Number Theory 15 (2019), 1863-1893.
• Z.-W. Sun, "Various Refinements of Lagrange's Four-Square Theorem," Westlake Number Theory Symposium, Nanjing University, China, 2020.
• S. Banerjee, "On a conjecture of Sun about sums of restricted squares," J. Number Theory 256 (2024), 253-289.

def OeisA308734.IsSumOfFourSquaresWithPowers (n : ℕ) : Prop

The predicate that n can be written as $(2^a \cdot 3^b)^2 + (2^c \cdot 5^d)^2 + x^2 + y^2$ for nonnegative integers $a, b, c, d, x, y$.

Equations

• OeisA308734.IsSumOfFourSquaresWithPowers n = ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (x : ℕ) (y : ℕ), n = (2 ^ a * 3 ^ b) ^ 2 + (2 ^ c * 5 ^ d) ^ 2 + x ^ 2 + y ^ 2

theorem OeisA308734.isSumOfFourSquaresWithPowers_2 : IsSumOfFourSquaresWithPowers 2

theorem OeisA308734.isSumOfFourSquaresWithPowers_3 : IsSumOfFourSquaresWithPowers 3

theorem OeisA308734.isSumOfFourSquaresWithPowers_5 : IsSumOfFourSquaresWithPowers 5

theorem OeisA308734.conjecture (n : ℕ) (hn : 1 < n) : IsSumOfFourSquaresWithPowers n

Zhi-Wei Sun's Four-Square Conjecture (A308734): Any integer $n > 1$ can be written as $(2^a \cdot 3^b)^2 + (2^c \cdot 5^d)^2 + x^2 + y^2$ for nonnegative integers $a, b, c, d, x, y$.