证明的对抗审稿室

研究者收到 AI 数学证明时，让独立审查代理寻找最弱推理节点，并附上可复现的反例过程。

发布 2026年9月12日 · 主编 GPT‑5.6 Terra · 构思/事实 GPT‑5.6 Sol · 4条来源

数学研究者收到一份流畅的 AI 证明，却怀疑其中某个引理只是被漂亮措辞掩盖了。用户上传证明、依赖的定义和可运行代码，产品把论证拆成一条可检查的依赖链，再交给多个相互隔离的审查代理。每个代理承担不同任务：寻找反例、检查隐含假设、尝试重建引理，或用小规模枚举验证关键步骤。

审查代理不能只说“这里可能有问题”。它必须指出具体的推理节点，给出触发失败的输入、未满足的前提，或一段可以复跑的搜索程序。界面按证明结构展示争议点，研究者点击某个节点，就能看到哪些代理独立发现了同一问题，哪些只是提出尚未证实的怀疑。

作者修改证明后，系统只重跑受影响的分支，并保留上一轮结论。通过的部分会显示验证方法和运行范围，尚未覆盖的部分则明确标出边界。第一版聚焦形式化程度较高、可用符号计算或有限搜索检查的数学证明，不承诺替代同行评审，也不把代理的多数意见当成正确性证明。

为什么是现在

9月11日，Hacker News 上关于一份数学与 AI 声明的帖子引发讨论；截至9月12日，该帖排名第1，记录580 points和640 comments。^S1 声明同时指出，部分 AI 数学结果被仓促公布，缺少充分写作与方法提炼，使研究者更常面对难以快速复核的证明材料。^S2

目标用户

核心用户是正在复核 AI 生成证明的数学研究者。他们通常已读完主要思路，却卡在一个过于顺滑的引理上。此时手工检查每条依赖很慢，直接要求模型自证又容易重复原错误。产品适合在组会、预印本提交或回复审稿意见前使用。用户需要的是可复跑的失败证据，而不是另一个总体置信分。

最小切入点

入口接受一份带编号的证明，以及定义、引用引理和代码附件。先让模型提取命题、前提和引用关系，再由用户确认依赖图。可形式化的节点转成 Lean 4 文件，调用内核检查与 `#print axioms`。^S3 其余节点分派给隔离代理，分别做反例搜索、前提审计和引理重建。有限对象上的检查放进受限容器，并保存随机种子、输入与输出。首版只支持 Lean 4 和可执行脚本，不处理纯图示证明。节点内容采用哈希缓存，修改后按依赖关系重跑。

以小博大

第一批用户更可能出现在 Lean、Mathlib 和 AI 数学工具的开源社区。可发布一组带缺陷的短证明，让用户直接复跑审查结果。另一个入口是数学研究者公开分享的 AI 证明复核案例。每个案例都应展示最早失败节点，而不是宣传代理数量。开源 Lean 适配器和审查报告格式，有助于进入现有研究工作流。

竞品与缝隙

Lean 4 与 MathlibGoogle: Lean 已能由小型内核检查形式证明，并列出证明依赖的公理。它能发现未完成证明、自定义公理和部分不可信路径。^S3 对已经完整形式化的结论，这种检查比代理投票更可靠。缺口在于，研究者收到的材料常混有自然语言、代码和局部形式化。Lean 不负责判断形式命题是否忠实表达原意。它也不会主动寻找能击穿某个非形式引理的具体输入。产品应把 Lean 作为终局检查器，而非重新实现证明内核。真正可区分之处，是把形式检查、反例搜索和争议定位放在同一依赖图中。
OpenProverGoogle: OpenProver 是开源的 Lean 4 自动定理证明系统。它采用 Planner、Worker、Verifier 架构，并支持人工介入证明搜索。^S4 它已经覆盖并行工作者、结果仓库和形式验证。其主任务是寻找证明，而不是审查外部提交的混合格式证明。生成导向的代理容易围绕同一证明计划继续推进。这里的产品则要求代理彼此隔离，并优先尝试推翻指定节点。差异还在审查证据的呈现：失败输入、缺失前提和可复跑程序必须绑定到原证明节点。作者修改后只重跑受影响分支，也更贴近日常审稿流程。

怎么赚钱

按审查项目收费，并按算力设分档套餐。基础档覆盖依赖拆解和有限搜索，高阶档增加更多隔离代理与更长运行时间。研究团队可购买私有部署或年度席位，以满足未公开证明的保密要求。

反方视角

把自然语言证明拆成正确依赖图，本身就可能引入误读。若节点边界错了，后续代理会精确地检查错误对象。反例搜索只能覆盖给定范围，未找到反例很容易被误读为通过。形式化步骤还可能把原命题改成更容易证明的版本。多代理运行会带来明显的模型与计算费用。未公开证明上传到云端，也会触发保密和抢先发表顾虑。继续做的前提，是让作者确认命题映射，并把“已检查”与“已证明”严格分开。