Lean 4

Van der Waerden number w(2;3,21)=416 proved with AI-assisted Lean proof

The long-open van der Waerden number w(2;3,21) is proved to equal 416, with the proof kernel-checked in Lean 4. Kullmann conjectured the value in 2010; the proof spans 209 cases and about 38.7 million leaf formulas, each refutation verified by cake_pr, an LRAT checker verified in CakeML and then bound by digest to its Lean term. It was produced by Hupyy's neuro-symbolic LPM system.