A.I. 日报
数学家借助AI证明范德瓦尔登数w(2;3,21)=416
一个长期悬而未决的范德瓦尔登数w(2;3,21)被证明等于416，证明经Lean 4内核校验。该值由Kullmann于2010年提出猜想，此次证明复盖209个案例、约3866万个叶公式，每个反证均由经CakeML验证的LRAT检查器cake_pr核验。证明由Hupyy的神经符号系统LPM生成，仅被Lean内核或cake_pr接受的步骤才计入。
AI 日报收录的 Lean 4 相关报道，共 1 篇，按时间倒序，每小时更新。
数学家借助AI证明范德瓦尔登数w(2;3,21)=416一个长期悬而未决的范德瓦尔登数w(2;3,21)被证明等于416，证明经Lean 4内核校验。该值由Kullmann于2010年提出猜想，此次证明复盖209个案例、约3866万个叶公式，每个反证均由经CakeML验证的LRAT检查器cake_pr核验。证明由Hupyy的神经符号系统LPM生成，仅被Lean内核或cake_pr接受的步骤才计入。