w(2;3,21) = 416, settled with LPM (Large Proof Model)

Resolving a conjecture of Kullmann from 2010, we prove that w(2;3,21) = 416: every red–blue colouring of 1, …, 416 contains a red three-term or a blue 21-term arithmetic progression, and some colouring of 1, …, 415 contains neither. Ahmed, Kullmann and Snevily restated the conjecture as open in 2014, and Google DeepMind's Formal Conjectures benchmark listed it as an open research conjecture in 2026. The proof was produced with LPM (Large Proof Model), a scalable neuro-symbolic reasoning system. Its agents wrote a Lean 4 development and ran the computation, and no formal step or refutation they produced was counted unless the Lean kernel or the proof checker cake_lpr accepted it. The result is a Lean theorem whose hypotheses state that 38,661,140 leaf formulas and the cover formulas of 209 cases and of 235,314 items in the 16 two-level cases are unsatisfiable; each refutation was checked by cake_lpr, and each file bound by digest to its Lean term outside the kernel. The same pipeline checks w(2;3,20) = 389, the value attributed to Kouřil (ParCo 2015).