Formal target: Corpus.OEIS280831.conjecture
**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.
Exact formal statement
∀ (n : Nat), Corpus.OEIS280831.A nThis target is a formal statement, not a proof of the problem.
Environment availability: available.