The 1680-Conjecture

Any nonnegative integer can be written as $x^2 + y^2 + z^2 + w^2$ with $x, y, z, w$ nonnegative integers such that $x^4 + 1680 y^3 z$ is a square.

Zhi-Wei Sun has offered a prize of 1,680 RMB for the first proof.

References:

• OEIS A280831
• Z.-W. Sun, "Refining Lagrange's four-square theorem," J. Number Theory 175 (2017), 167-190.
• Z.-W. Sun, "Refining Lagrange's four-square theorem," arXiv:1604.06723 [math.NT], 2016.

def OEIS.A280831.HasSquareCondition (n : ℕ) : Prop

The predicate that n can be written as $x^2 + y^2 + z^2 + w^2$ with $x, y, z, w$ nonnegative integers such that $x^4 + 1680 y^3 z$ is a square.

Equations

• OEIS.A280831.HasSquareCondition n = ∃ (x : ℕ) (y : ℕ) (z : ℕ) (w : ℕ), n = x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2 ∧ IsSquare (x ^ 4 + 1680 * y ^ 3 * z)

theorem OEIS.A280831.hasSquareCondition_0 : HasSquareCondition 0

theorem OEIS.A280831.hasSquareCondition_7 : HasSquareCondition 7

theorem OEIS.A280831.hasSquareCondition_95 : HasSquareCondition 95

theorem OEIS.A280831.conjecture (n : ℕ) : HasSquareCondition n

Zhi-Wei Sun's 1680-Conjecture (A280831): Any nonnegative integer can be written as $x^2 + y^2 + z^2 + w^2$ with $x, y, z, w$ nonnegative integers such that $x^4 + 1680 y^3 z$ is a square.