#AI
Vals 放出七点 Thomson 问题的双内核 Lean 证明
Vals AI 研究者发布一份「双内核校验」Lean 工件，针对七点 Thomson 问题。仓库称 Lean 与 nanoda 内核均接受。
仓库自注「陈述未经人类认证、未同行评审」;综述方未重跑构建、未获数学家认证。
做法是数值优化找证书系数、转精确数据交 Lean 检查；约 10 个 Claude Sonnet 5.5 agent 跑约 15 小时，产出 17895 行文档。
💡 为什么值得看两个独立内核都过了，看点在其诚实度。
查证
来源档案
Ground Truth
以「验证延迟」为报道主线的小型新闻站，本篇是对 Vals 一手仓库与作者写法的综述与复述，非独立复现。
转述链条清楚，并主动标注了两处边界：未重跑构建、未获数学家认证。仓库内所有校验结论目前仍是作者自述，无第二方独立复现。
延伸阅读
复核 17895 行 Lean 文档、Comparator 与 nanoda 的接受记录，以及负向对照是否可复现。
两个固定 Lean 定理陈述加以受控的方式锁定目标，是在防 agent 悄悄改题，这条工程约束比证明本身更可复用。