Vals AI 用 10 个 Claude Sonnet 5.5 agents 完成 Thomson problem N=7 的 17,895 行 Lean 证明

Vals AI 报告让 10 个 Claude Sonnet 5.5 agents 并行研究 Thomson problem 在 N=7 时的最优构型，约 15 小时后生成 17,895 行 Lean 证明，证明正五角双锥是七个单位电荷在球面上的最低能量构型。官方博客称该证明被 Lean 接受，并由第二个 kernel 实现复核；它把多 agent 数学搜索、长形式证明生成与 kernel verification 串成一次公开实验。