Research
Proof confirms van der Waerden number W(2;3,21) equals 416, checked in Lean 4
The result was produced with LPM, a neuro-symbolic system from Hupyy, and verified by the Lean kernel and the cake_pr LRAT checker. The conjecture dates to Kullmann in 2010 and was listed as open by DeepMind's Formal Conjectures this year.