AREX Feed Article
Vals AI 称 10 个 Claude Sonnet 5.5 agent 在 15 小时内完成 Thomson 问题 N=7 的 Lean 证明，结论为正五角双锥
9 月 29 日（协调世界时 02:16，北京时间 10:16），LLM 评测机构 Vals AI 在 X 上发布称，它让 10 个 Claude Sonnet 5.5 agent（智能体）用定理证明器 Lean 4 完成了球面上 7 个电子最低能排列（Thomson 问题 N=7）的形式化证明：约 15 小时内产出 17,895 行，被 Lean kernel（Lean 的证明检查内核）接受，结论是正五角双锥——五个电子沿赤道排成一圈、两极各有一个。
在后续帖文里，Vals AI 给出了和的链接；仓库里放着证明文件、论文、复现说明和验证记录。Vals AI 的主业是对领先 AI 模型的公开评测，其自我描述为“独立评测、无偏基准”（Independent Evaluation, Unbiased Benchmarks）。
一块消息板、1,270 条消息和一个整合者
按照 Vals AI 博客的记录，实验的起点是一块消息板和一个 Lean 项目：10 个 Claude Sonnet 5.5 agent 以最高推理强度（maximum effort）运行，在消息板上写下了 1,270 条消息。
要证的东西被预先固定成两条 Lean 语句，放在挑战文件里（仓库中对应文件里的定理还挂着 sorry，这是 Lean 里表示尚未证明的占位符）。博客说，任务书提出九个方向（移植 N=8 的先例、线性规划界、按组合类型切分、构建可验证的证书引擎等），agent 可以放弃或合并方向，但要说明理由；它们必须只用 Lean 的标准公理完成 kernel 检查。
最终有一个 agent 认领了“整合者”角色，把已验证的片段合并进同一个证明文件。按博客的规则，候选证明只有在通过检查器之后才算数：可复现的 Lean 构建、针对固定挑战文件的 Comparator 比对、公理检查。
在帖文回复中，用户 John Rood（）把 10 个 agent 同做一个证明的可行性归因于 Lean 的机制：每个引理都有机器给出的裁决、不需要人在回路中，“并行猜测只在机器能够完整检查的范围内才安全”。
五道检查与一次故意改错的负对照
博客的“形式化验证”一节列出五道检查，验证日志随仓库一起公开：
- 从干净副本构建：通过；599 秒墙钟时间，其中
lake build用 344 秒、跑了 8,928 个任务； - 公理检查：
#print axioms显示两个定理只依赖 Lean 的标准公理 propext、Classical.choice 与 Quot.sound； - Lean Comparator（比较器）：确认解决方案恰好证明了挑战文件里的固定语句，返回“Your solution is okay!”（解答通过），耗时 260 秒；
- 第二个 kernel：把证明导出后交给另一套 kernel 实现 nanoda 检查，47,854 个声明全部通过；
- 负对照：把 Case 1 数据里的一个整数改掉，nanoda 随即中止。
博客称，证明的每一步都由 kernel 内精确的整数或有理数运算完成，不依赖浮点数或数值表。证明是单文件 Solution.lean，仅导入 Mathlib（Lean 的数学库）。
一个最小内积，把构型空间切成一个球冠和五块条带
据 Vals AI 博客，证明按两点间最小内积 m 把全部构型切成两组情形：m ≥ -0.90 的 Case 1，以及 m < -0.90 的 Case 2；后者再被分为一个球冠和五块条带，每一块都有明确的数据证书：
- Case 1（不存在几乎对跖的点对）：由一个五次（degree-5）的三点式半正定规划（SDP）界处理（属 Bachoc–Vallentin 类型，由 Cohn 与 Woo 适配到能量问题），并配一个多项式下界，严格余量为 E ≥ E(P) + 3/10000；
- 五块条带
[-0.99, -0.98]、[-0.98, -0.96]、[-0.96, -0.94]、[-0.94, -0.93]、[-0.93, -0.90]：每块由一份带类型的三点式证书排除，严格余量约 2.6e-6； - 球冠（cap，m ∈ [-1, -0.99]，包含正五角双锥本身）：一份“近锐”证书把任何竞争者限制在正五角双锥附近，与最低能量 E(P) 的差不超过 2.3e-16；随后区间算术的刚性论证与精确的二阶局部极小性定理给出 E ≥ E(P) 与唯一性。
证明的两个主定理在 Lean 里叫 thomson_seven 与 thomson_seven_unique：前者说正五角双锥的能量不高于任何其他构型；后者说，取等号时构型只能是正五角双锥经过旋转、镜像和重编号后的样子。正五角双锥的能量 E(P) = 14.4529774142…。证书先用数值半正定规划寻找、再取整为精确数字；博客强调，Lean 检查的是这些数字本身，因此证明不依赖于找到它们的求解器。最后把球冠、五块条带与 Case 1 三部分拼到一起，只用了五行。
Thomson 问题与它前面的 N=8 结果
Thomson 问题问的是：把 N 个互相排斥的电荷放在球面上，怎样排布总能量最低。对 N=7，按 Vals AI 的说法，数值计算几十年来一直指向同一个答案；难的是排除其余所有排布，因为构型空间是连续的。Vals AI 还称，这道题此前始终没有证明，严格证明只存在于少数几个小 N 上。
N=7 的这次证明建立在 9 月发布的 N=8 结果上。9 月 18 日提交到 arXiv 的论文《Energy minimization for eight points on the sphere》（作者为 Liudmyla Kryvonos、Lukas Liehr 与 Mitchell A. Taylor）证明，在全等（congruence）意义下 N=8 的唯一极小构型是某个特定高度的方形反棱柱（square antiprism），这份证明是计算机辅助的，并已在 Lean 中完整验证（）；N=8 的 Lean 开发则见 Joseph Tooby-Smith 与 Alex Zughaid 的 。按 Vals AI 博客的说法，N=7 的这次证明把 N=8 背后的三点法带了过来，再加上按最小内积的切分、分别处理两极与赤道的带类型证书，以及在正五角双锥处的精确二阶论证。
能复跑的机器检查，与仓库自己标注的边界
仓库把整条验证链放在同一处：Solution.lean（两个主定理排在文件末尾）、论文 PDF 与 Markdown 源文件、论文论证到 Lean 行号的映射表、REPRODUCE.md 与检查脚本、验证日志，以及哈希校验文件；构建锁定在 Lean v4.34.1 和一个固定 commit 的 Mathlib 上。
按仓库的复现说明，机器检查可以在干净副本上重跑：构建、Comparator 比对、nanoda 独立检查，脚本与日志都在仓库里。对于这份证明的认证状态，仓库说明栏的标注是：“Statement not human-certified. Not peer reviewed.”（未经人工认证，未经同行评审）。