2026-09-05
哥大等提出 Prove2Me：人只审核心命题，Agent 用 proof-sketch 拆引理、互相引用写 Lean。Bandit Algorithms 教材 15.1 万行、6 个 Agent、约 400 美元、13 天收工。案例研究，不是对照实验。
Lean 4 能把数学证到机器可检查，但门槛是同时懂数学和证明助手。Scholze 的 Liquid Tensor Experiment 社区干了大约十八个月；Buzzard 领的费马大定理形式化计划五年，他自己说一个人做不完。AI 证明器已经能写复杂 Lean，可现有项目仍卡在三处：人审跟不上动辄十万条定理的生成；GitHub 上的库互相缠死，单条结果很难抽出来复用；大规模 agent 蜂群绑在一家机构的内部算力上。
Prove2Me 要把形式化做成任何人带一个能跑终端的 Agent 就能来的众包。注意：中文圈讨论里那条「Claude 十一天形式化费马、一千三百万行 Lean」不是这篇的结果。这篇只把费马项目当动机，自己跑的是矩阵补全、复杂度定理和几本教材。
命题和证明拆开。每条定理是不可变对象，声明以 sorry 占位；证明提交必须类型完全匹配、无 sorry、无新公理，由平台选定的 Lean 内核验收。人当 captain 发起 mission：头条目标、依赖定义、里程碑引理构成受审核心，中间引理放开给 Agent 长。忠实性用独立审核 Agent 做回读：只看 Lean，译回自然语言，再和来源对照，captain 不必自己读完证明助手代码。
协作的核心是 proof-sketch：一份无 sorry 的证明可以 import 平台上其他定理，包括还没被证的。Huang 的 Sensitivity Conjecture 被拆成度数界、Cauchy 交错、矩阵谱等子题，子题证完父定理自动闭合。同一套 import 也让已证结果变成 Formalpedia 里可检索、可引用的积木。里程碑是 captain 从原文抄下来的权威陈述，防止并行 Agent 把同一条引理形式化成互不兼容的版本。讨论区里 Agent 会互相纠错：有一条 gotsmanlinial 被证伪后，补上边界条件才把那一支关上。
接入方式是让 Agent 去读 prove2.me/start.md。网页聊天机器人不行，因为要跑代码调 API。
2026 年 6 月中到 7 月底的案例，不是受控实验。代价口径也不统一：对照那行是按 API 计量，Prove2Me 几行按消费级包月约 200 美元乘人数估算。
| Mission | 类型 | Lean 行数 | 代价 | Agent 数 | 天数 |
| Algebraic Combinatorics（Gloeckle 等对照） | 教材 | 13.0 万 | 约 10 万美元 API | 3 万 | 7 |
| Exact Matrix Completion | 论文 | 8.1 万 | 约 600 美元 | 9 | 16 |
| Sipser–Gács–Lautemann | 论文 | 5.5 万 | 约 400 美元 | 3 | 8 |
| Bandit Algorithms | 教材 | 15.1 万 | 约 400 美元 | 6 | 13 |
| Introduction to Linear Optimization | 教材 | 1.7 万 | 约 200 美元 | 4 | 7 |
最大的 Prove2Me 任务 15.1 万行，体量接近那次 13 万行的中心化蜂群，但只有 6 个 Agent、两个订阅。Sensitivity Conjecture 作为贯穿例子也收了，四个里程碑都打上。作者写明：更强模型和为多 Agent 证明设计的 harness 混在每一行里，单靠这张表分不开。
形式化的单位从「一个实验室的 Git 仓库」变成「一条可独立 import 的定理」。对人，审的是核心命题像不像原意；对 Agent，机械劳动可以拆开并行。消费级订阅能堆出十万行级 Lean，说明瓶颈从算力账单挪到了审核协议和检索。
作者自己把表 1 降级为案例。模型代际和 harness 混杂，没有「固定模型只改平台」的对照。人仍必须审核心，规模一大，captain 和平台管理员会成为新瓶颈。Lean 过核不等于语义忠实，文中引用的 Lean-as-judge 审计大约只有 43% 的已证命题过关。去中心、异步 Agent 怎么协调，正文写成未解问题。Formalpedia 变大之后，如何找到该 import 的那一条，也还没有评测。