Lean 4 theorem proves W(2;3,21) equals 416 using neuro-symbolic system
A neuro-symbolic system has formally proven the van der Waerden number W(2;3,21)=416, with the result verified by the Lean 4 kernel and cake_pr.
Lean 4 theorem $W(2;3,21) = 416$ is proven and checked by the Lean kernel, settling a value Oliver Kullmann conjectured in 2010. Every red-blue colouring of the integers from 1 to 416 contains a red 3-term arithmetic progression or a blue 21-term arithmetic progression, while some colouring of integers from 1 to 415 contains neither. Google DeepMind's Formal Conjectures list previously carried this value as open.
The proof came from LPM, a neuro-symbolic system from Hupyy. Nothing counted toward the final result unless accepted by the Lean kernel or the cake_pr checker. The Lean 4 theorem divides the problem into 209 cases and 38,661,140 leaf formulas. Cake_pr, an LRAT proof checker verified in CakeML, checked a refutation for each leaf. Each refutation is bound by digest to its Lean term, tying external checker verdicts to the Lean kernel.
This leaves neural and search components outside the trusted base. The paper is published on Zenodo with DOI 10.5281/zenodo.23776306. A 13.6 GB evidence package containing Lean sources, checker records, and a replay kit is available at DOI 10.5281/zenodo.23749222. You can check package integrity by running shasum -a 256 -c SHA256SUMS. Because the work is released as a preprint, it has not necessarily undergone peer review, but the package lets independent parties replay the verification.