W(2;3,21) = 416 - a van der Waerden number conjectured by Kullmann in 2010, now proved with a Lean 4 kernel-checked proof [R]

w(2;3,21) = 416 - today proved with a Lean 4 kernel- checked proof (preprint + 13.6 GB evidence package). Every red-blue colouring of {1, ..., 416} contains a red 3-term or a blue 21-term arithmetic progression, and some colouring of {1, ..., 415} contains neither. Kullmann conjectured the value in 2010; DeepMind's Formal Conjectures list still carried it as open this year. The proof is a Lean 4 theorem over 209 cases and 38,661,140 leaf formulas, each refutation checked by cake_pr (the LRAT checker verified in CakeML) and bound by digest to its Lean term. It was produced with LPM (Large Proof