Mixed sums of four pentagonal numbers over the natural numbers: a conjecture of Sun

Let p5(x) = x(3x−1)/2 and p̄5(x) = x(3x+1)/2. Z.-W. Sun conjectured (J. Number Theory 162 (2016), Conjecture 5.2(i)) that both p5+p5+p̄5+p̄5 and p5+p5+p5+p̄5 are universal over the natural numbers: every n ≥ 0 is p5(w)+p5(x)+p̄5(y)+p̄5(z), and also p5(w)+p5(x)+p5(y)+p̄5(z), with w, x, y, z ≥ 0. We prove both statements. The problem becomes one about lattice points on spheres in a coset of 6Z⁴ with two (resp. three) negative coordinates. We detect them with explicit polynomial weights and bound the resulting theta series of level 144 and weights 2 to 11 through certified newform decompositions and Deligne's bound; for the second sum the odd-degree series carry the character (−3/·) and the polynomial inequality needs a new certificate. The remaining finitely many cases (n < 5·10⁸) are checked directly. The proof is computer-assisted. The mathematics, programs and text were produced by the AI system Claude (Anthropic) under the author's direction. Each sum was audited by a separate run of the same AI with its own code and re-verified without PARI/GP's modular-forms code (SageMath), the polynomial inequality was re-proved by a second algorithm, and the paper was reviewed adversarially by ChatGPT (OpenAI), which found no error. No human expert has yet checked the argument. The record contains the paper, all programs, certificates, logs, witness lists, the audits, the re-verifications and a guide to rerunning every computation.