Formal target: Corpus.OEIS303656.conjecture

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

Exact formal statement

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

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

Environment availability: available.