Vals AI 利用10个Claude智能体协作完成汤姆逊问题N=7的Lean形式化证明

Vals AI 通过组织10个Claude智能体协作15小时，生成了17895行Lean代码，成功完成了物理数学难题汤姆逊问题N=7的形式化证明。智能体在没有人工介入分工的情况下自主讨论、探索算法并合并代码，将构型空间分区结合精确代数运算，证明了五角双锥构型具有最低能量。该证明已通过Lean内核与独立内核nanoda的双重编译校验。