Lean 4验证范德瓦尔登数w(2;3,21)=416
原文：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——今天用 Lean 4 内核检查证明（预印本 + 13.6 GB 证据包）。{1, ..., 416} 的每一种红蓝着色都包含一个红色 3 项或蓝色 21 项等差数列，而 {1, ..., 415} 的某种着色两者都不包含。Kullmann 在 2010 年猜想了该值；DeepMind 的形式化猜想列表今年仍将其列为未解决。该证明是一个 Lean 4 定理，涵盖 209 个案例和 38,661,140 个叶公式，每个反驳都由 cake_pr（在 CakeML 中验证的 LRAT 检查器）检查，并通过摘要绑定到其 Lean 项。它由 Hupyy 的神经符号系统 LPM（Large Proof Model）生成；除非 Lean 内核或 cake_pr 接受，否则不计入。论文：https://doi.org/10.5281/zenodo.23776306 证据包（Lean 源码、检查器记录、重放工具包）：https://doi.org/10.5281/zenodo.23749222 检查方法：下载并运行 'shasum -a 256 -c SHA256SUMS'