Formal target: Corpus.OEIS308734.conjecture

**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$.

Exact formal statement

∀ (n : Nat), LT.lt.{0} 1 n → Corpus.OEIS308734.A n

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record