COMPUTER PROOF vs computer proof- Quadratic VDW theorem

Quad VDW Theorem: For all c there exists W=W(c) such that for all c-colorings of {1,...,W} there exists a,d such that a and a+d² are the same color. What is known about W(c)? The first proof of Quad VDW was nonconstructive. The second proof was constructive but used VDW's theorem and gave terrible bounds, even for W(2). EASY: Show W(2)=5 ON A HS MATH COMP: Show that for all 3-colorings of {1,...,2003} there exists two numbers a square apart that are the same color. One can get a bound less than 100. With a lot more detailed work one can get W(3)=29. None of above was done with a computer. SO- what about W(4)?  There are three proofs that W(4) exists: a) Prove the QUAD VDW theorem. This gives terrible bounds. b) I had some students use SAT solvers and they obtained W(4)=58. I am sure they are right and I am glad to know it (especially since it confirms the general mantra that the bounds from proofs in Ramsey theory tend to be much bigger than the reality) but its somehow unsatisfying. I want a HS proof. I wanted to put it on the MD Math Comp for 2017 but wiser people prevailed. c) I gave the problem to a Grad Student Zach Price and he came up with a HS proof-- sort of.  Look at the following graph: here.  It shows that in any 4-coloring of N which does not have two numbers a square apart the same color: COL(x) = COL(x+290085289) from this one can obtain W(4) ≤ 290085289²  (which is MUCH better than the bound from the proof of Quad VDW) and hence a proof of QVDW that does not need a program, except that to FIND this gadget used a program.  I doubt a HS student could do this on an exam. Is Zach's proof the HS proof I am looking for? PRO- once you see it its easy to verify and does not need a program. CON- coming up with it needed a program. More to the point: which proof do you like better: 1) The SAT Solver proof.  Not a proof you can see or feel, but gives exact bounds. or 2) Zach's gadget proof. Much worse bound but you can see and feel the proof, and verify it after you know the gadget. I prefer Zach's proof.