报道：Lean 4证明确定W(2;3,21)为416
一篇报道称，W(2;3,21) = 416已通过Lean 4内核检查的证明得到证明，解决了Kullmann于2010年提出的猜想。该定理涵盖209个案例和38,661,140个叶公式，每个反例均由cake_pr检查，并通过摘要绑定到对应的Lean项。证明由Hupyy的神经符号Large Proof Model生成；报道指出，只有通过Lean内核或cake_pr接受的内容才被计入。
据报道，这一结果以机器检查方式解决了今年早些时候仍列在DeepMind“Formal Conjectures”清单中的组合数学猜想，同时展示了神经符号证明模型在形式验证约束下的实际应用。
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 Model), a neuro-symbolic system from Hupyy; nothing counted unless the Lean kernel or cake_pr accepted it.
Paper: https://doi.org/10.5281/zenodo.23776306
Evidence package (Lean sources, checker records, replay kit): https://doi.org/10.5281/zenodo.23749222
To check: download it and run 'shasum -a 256 -c SHA256SUMS'
submitted by /u/Rodriguez909 [link] [comments]