Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng
cs.AI, cs.LO, cs.MA
2026-08-28
Columbia等推出Prove2Me，把定理陈述与证明拆开，用proof-sketch把大定理拆成可独立提交的子问题。Bandit Algorithms教材形式化写出15.1万行Lean，6个Agent、约400美元订阅、13天完成。
Lean 4 能把定理变成机器可检查的对象,大规模形式化却一直卡在人身上。Scholze 的 Liquid Tensor Experiment 花了大约 18 个月社区协作;Buzzard 领衔的费马大定理形式化按 5 年资助规划,他自己说「没法一个人做完」。AI 已经能把教材和论文往 Lean 里推,可三个问题还在:陈述是否忠实于原意,人审不过来;GitHub 上一整库互相耦合的定理很难单独拿出来复用;大规模 swarm 跑在单一机构的内部算力上,外面的人进不去。
Prove2Me 想把形式化做成带一个 Agent 就能参与的众包:人只审一小块核心陈述,Agent 去填证明细节,证明之间还能互相引用。
平台把定理和证明拆成两类不可变对象。定理卡片含自然语言说明、preamble、以 sorry 结尾的 Lean 陈述;证明提交必须声明名为 solution 的定理,类型与目标完全一致,且不含 sorry 或新公理。后端按 Curry-Howard 对应检查类型是否匹配,也可以提交否定陈述当反证。
人审被限制在「任务」(mission)的核心:目标定理、依赖定义、里程碑引理。船长不必会写 Lean,但必须逐条点击确认。为了让不会读 Lean 的人也能审,独立 auditor Agent 做 read-back:只看 Lean 声明、不看原文,把它译回 LaTeX,人拿两段数学陈述对照。Bourigault 等人用 Lean-as-judge 审过,只有约 43% 的已证陈述被判忠实,所以这个人工门不能省。
协作靠 proof-sketch:一份不含 sorry 的证明可以 import 平台上其他定理,包括还没被证明的。父定理的 sketch 被接受后,子引理变成独立题目;子引理证完,父定理自动闭合。不可变性保证局部正确性能拼成全局正确。里程碑把源论文里的关键引理钉成权威陈述,避免多个 Agent 把同一条引理形式化成互相不能 import 的版本。证完的原子定理进入 Formalpedia,带搜索 API,后来的 sketch 可以直接引用。贡献者的积分既奖励闭合开放定理,也奖励被别人 import 的陈述。
2026 年 6 月中到 7 月底的案例,论文自己标明不是对照实验:
| 任务 | 类型 | Lean 行数 | 成本口径 | Agent 数 | 天数 |
| Gloeckle 等代数组合教材(外部对照) | 教材 | 13 万 | API 约 10 万美元 | 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 |
最大一档 15.1 万行,体量跟那次 13 万行的中心化 swarm 接近,但只用了 6 个 Agent、两份消费级订阅。Sensitivity Conjecture 任务的四个里程碑全部闭合。API 计费和包月订阅不在同一口径,不能直接比谁更便宜。
写 Lean 的门槛从「会证明助手」降到「会用自然语言指挥 Agent」。对想把论文或教材形式化的人,mission 把审计面锁在核心陈述上,中间引理可以放开生成。Formalpedia 让一次形式化的副产品能被下次任务直接 import,这是 Git 整库发布做不到的。
这是工程与机制设计,不是新的定理证明模型。平台不声称比 AlphaProof 更会证题。
案例研究自己写明:语料难度、工作方式和模型代数混在一起,无法拆开「更强模型」和「harness」各自贡献了多少。订阅费用按人数×约 200 美元/月估算,和 Gloeckle 等的 API 账单不对齐。
人仍然必须审 mission 核心,陈述忠实性没有可扩展的自动保证。开放提交会引入低质量甚至对抗内容,声誉系统还在愿景里。去中心、异步的多 Agent 如何交换上下文,论文当成开放问题。选什么值得形式化、里程碑怎么切,仍然是人的判断。