如果让一群 AI 证明数学定理，我们需要设计一家怎样的“公司”？

（本文是我最近阅读许多AI证明数学问题后想到的，之前我一直觉得Agents的下一步可能是需要自我博弈提升，但是似乎现在可以跳过这一步，直接用人类的管理学、公司制度去组织Agents，我和codex讨论后就有了这个文章）

假设你拥有 16 个、128 个，甚至几千个能力很强的 AI Agent，任务是攻克一个重要数学问题。

最自然的想法可能是：让所有 Agent 各自尝试证明，最后把答案汇总起来，选择看起来最好的一份。

但这个方法大概率不会得到 16 倍、128 倍的智能。它更可能得到大量重复的猜想、彼此污染的推理、无法追踪的聊天记录，以及一份所有 Agent 都觉得正确、实际上藏着同一个漏洞的证明。

当 Agent 数量增加以后，真正稀缺的已经不再是“再生成一种思路”的能力，而是：

• 怎样把一个未知问题拆成可以研究的中间问题？
• 怎样保持不同研究路线的独立性？
• 怎样判断一个中间结论是否真的成立？
• 怎样让错误结论不会污染整个系统？
• 怎样把分散的正确结果重新组合成完整证明？
• 人类应该在什么时候介入？

这时，问题已经不只是多智能体推理，而开始接近组织设计。

我们需要建设的不是一个“大群聊”，而是一家专门生产数学知识的 AI 公司，或者更准确地说，一套 AI 数学证明组织系统。

一、这家公司的产品不是答案，而是可验证的数学对象

普通办公软件的基本对象是消息、文档、任务和会议。AI 数学证明系统的基本对象则应该是：

• 命题（Claim）
• 证明（Proof）
• 反例（Counterexample）
• 证明义务（Proof Obligation）
• 依赖关系（Dependency）
• 审查意见（Review）
• 研究决策（Decision）

例如，一个 Agent 不能只汇报：

我发现稀疏化可能保留 END-OF-LINE 的某种奇偶结构，这条路线似乎很有前景。

它必须提交一个可以被其他 Agent 攻击的对象：

Claim ID：CLAIM-0042
精确命题：变换 S 在条件 A、B 下保持端点奇偶性
使用的定义：DEF-0011、DEF-0018
依赖的引理：CLAIM-0027
当前证明：PROOF-0042-v2
尚未解决：步骤 7 的位复杂度界
建议攻击方向：构造非单射映射的最小反例

这条规则看起来只是格式要求，实际上改变了整个组织的性质。

Agent 不再通过“谁说得更有道理”协作，而是通过可以追踪、攻击、复现和组合的数学对象协作。

聊天只是工作过程，Claim 才是组织资产。

二、一个 16-Agent 数学研究所

一开始没有必要组织 128 个 Agent。更合理的做法是先建立一个 16-Agent 的最小研究所，验证组织制度本身是否有效。

它可以这样分工：

这里真正意义上的“行政人员”只有调度 Agent。知识管理员和科学编辑也必须理解数学，只是它们不以提出新定理为主要目标。

八个研究员可以来自不同模型家族。例如，一部分擅长长上下文和整体结构，一部分适合低成本并行探索，一部分更擅长形式化代码。模型异构不是采购策略，而是科学可靠性的一部分。

如果所有 Agent 都来自同一个模型，它们很可能拥有相同的知识盲点、推理习惯和奖励偏好。十个高度相关的判断，并不等于十份独立证据。

三、组织结构：大学、市场和法院的混合体

这套组织不能只像公司，也不能只像学校。它更接近三个制度的组合。

1. 大学：保护异质探索

研究初期，同一问题交给多个团队盲态研究。它们看得到共同定义和公开文献，但暂时看不到其他团队的猜想。

这样做是为了防止所有 Agent 过早收敛到第一条看起来合理的路线。

系统甚至可以故意建立不同“学派”：

• 一个团队只研究组合结构
• 一个团队从拓扑和不动点出发
• 一个团队研究电路、查询或证明复杂度
• 一个团队专门尝试设计算法，反驳“这个问题一定很难”的直觉

算法团队尤其重要。一个以证明下界为目标的组织，如果没有人认真寻找算法，很容易把所有实验现象都解释成困难性证据。

2. 市场：让资源跟随证据流动

Agent 不永久属于某条路线，而是获得有限租约。

一个研究周期结束后，路线根据产物进入不同状态：

• 绿色：产生了经过独立验证的新引理，继续获得资源
• 黄色：有进展，但未验证假设增长，停止扩编并接受攻击
• 灰色：连续多个周期没有可检查产物，暂时冻结
• 红色：核心命题被反例推翻，立即停止下游使用

资源不能根据 Agent 的自信程度分配，而要根据证据分配。

一个非常会写报告的 Agent，不应该比一个找到关键反例但表达朴素的 Agent 获得更多资源。

3. 法院：证明的提出者不能兼任裁判

任何重要结论都要经过三道相互独立的程序：

1. 对抗审查：专门寻找反例、量词错误和隐含假设。
2. 盲态重建：不读原始聊天，只根据正式命题从零证明。
3. 形式化检查：把最关键的定义和推导交给证明助手。

这里不能采用多数投票。

十二个 Agent 都认为证明正确，并不能让一个错误步骤变正确。数学组织最终依赖的是可重建的证明关系，而不是共识。

四、AI 数学证明系统的十二条基本规则

如果要给这家研究所写一部“公司章程”，我会从下面十二条开始。

规则一：Claim 优先于聊天

任何值得被其他团队依赖的结论，都必须转化为有版本号的 Claim。聊天记录不能作为数学依据。

规则二：提出者不能批准自己的结论

研究 Agent 可以提交证明，但无权把它标记为“已经成立”。

规则三：共识不是证明

Agent 数量、模型声望和置信度不能替代逐步验证。

规则四：独立思考发生在交流之前

重要问题先由不同模型或不同上下文的 Agent 独立尝试，再交换结果。过早交流会破坏认知多样性。

规则五：失败结果也是组织资产

反例、失败归约、走不通的方法和已知障碍必须保存。后续 Agent 应该能够查询“为什么这条路上次失败了”。

规则六：上游失效必须自动向下传播

一个 Claim 被推翻后，所有依赖它的证明自动转为待复查，不能继续以旧状态流通。

规则七：每条路线都有租约和退出条件

不存在无限期的“继续深入研究”。路线必须提前说明下一项可证伪目标，以及什么结果意味着应该停止。

规则八：证明债务必须可见

系统持续统计未验证引理、隐含假设、失败复现和循环依赖。一个证明越长，不代表它越接近完成，也可能只是积累了更多债务。

规则九：不同模型承担不同认识论角色

擅长创造的模型不一定适合审稿；擅长长程写作的模型不一定适合寻找最小反例。角色根据内部测试动态调整，不能永久按照厂商宣传固定。

规则十：人类监督例外，而不是监督每一步

普通任务分配、Claim 创建和独立审查可以自动进行。修改最高目标、大幅提高预算、宣布主定理成立和对外发布必须由人类批准。

规则十一：所有重要操作可回放

谁在什么时候修改了命题、推翻了哪个引理、暂停了哪条路线，都进入不可覆盖的事件日志。

规则十二：论文不是事实来源

论文只是对已验证 Claim 的叙事组织。写作 Agent 不能为了行文流畅，在正文中偷偷改变数学命题。

五、Agent 之间应该怎样通信？

如果 16 个 Agent 彼此自由聊天，尚且可能管理；如果扩大到 128 个，通信关系会迅速失控。

因此，跨团队交流应该围绕对象，而不是围绕群聊。

围绕 CLAIM-0042 的讨论
围绕 NEED-0017 的中间需求
围绕 REVIEW-0021 的证明争议
围绕 TASK-0108 的工作交接

每个 Agent 只订阅：

• 自己当前研究的 Claim
• 直接上游依赖
• 直接下游使用者
• 与自己方向相邻的少量研究主题

系统还需要自动发现异常通信结构：

• 某个 Agent 是否成为所有信息的瓶颈？
• 一组 Agent 是否形成了只在内部互相认可的封闭小圈子？
• 是否所有验证都来自同一个模型家族？
• 是否大量 token 花在重复解释同一个命题？
• 是否有团队仍在引用已经失效的旧版本？

理想状态下，人类看到的不是几万条消息，而是一张实时变化的证明依赖图和一份异常清单。

六、新的中间问题从哪里获得人手？

数学研究不可能在开始时完成全部任务拆解。真正重要的中间引理，往往是在研究过程中才出现。

任何 Agent 都可以提交一个中间需求，但必须写清楚：

需要证明或推翻什么？
它阻塞哪一个主命题？
依赖哪些已经验证的结果？
什么产物算完成？
如果失败，能排除什么？

调度系统先派一个小型机动组进行短期侦察。如果这个需求同时阻塞多条高证据路线，就从停滞路线回收 Agent，成立临时项目。

中间问题解决后，临时项目立即解散。它不能因为已经形成团队，就不断为自己寻找新的存在理由。

这和现实公司的一个常见问题完全一致：组织容易从“为任务而存在”，逐渐变成“为了维持组织而制造任务”。AI 组织同样需要防止部门自我延续。

七、人类在其中做什么？

人类不应该每天阅读所有 Agent 的推理，也不应该审批每一次任务分配。否则人类会成为整套系统最慢的组件。

人类更适合承担四种职责：

1. 确定最高研究目标和不可突破的边界。
2. 决定预算、模型供应商和重大资源调整。
3. 处理两个独立验证系统无法解决的认识论争议。
4. 批准主定理的宣布和对外发布。

人类控制台只需要重点展示：

核心 Claim 可能存在反例
两个模型家族给出相反审查结论
某条路线成本异常增长
大量下游结果依赖一个未验证引理
候选定理已经通过两次独立重建

人类不是流水线上的质检员，而是研究所所长、制度设计者和最终出版人。

八、怎样评价这家 AI 公司是否真的在进步？

不能使用下面这些指标：

• 生成了多少 token
• 创建了多少任务
• 开了多少次 Agent 会议
• 提出了多少猜想
• 有多少 Agent 表示同意

更有意义的指标是：

• 单位成本产生的独立验证 Claim 数量
• 关键 Claim 的独立复现成功率
• 从提出命题到发现反例的平均时间
• 证明债务是增长还是下降
• 重复研究占总消耗的比例
• 不同模型家族之间的有效交叉审查率
• 失败路线留下了多少可复用信息

对于真正困难的数学问题，一个月没有得到完整证明并不意味着组织失败。但如果一个月以后只留下大量对话，没有留下可验证的引理、反例和障碍地图，这个组织就是失败的。

九、以 PPAD 为例，这套系统会怎样运行？

严格来说，PPAD 是一个复杂性类别，不是一个可以直接“证明”的命题。我们可以把最高目标具体化为研究 FP 与 PPAD 的关系，或者证明某个新问题具有 PPAD-complete 性质。

系统先把目标拆成几条相互独立的研究计划：

• END-OF-LINE 的图结构和电路表示
• Brouwer、Sperner 与组合拓扑路线
• 查询、电路和证明复杂度下界
• 新归约和新的完全问题
• 特殊结构下的多项式算法

假设拓扑团队提出 Claim：某种离散化保持奇偶端点结构。

系统不会立刻把它写进主证明，而会依次发生：

拓扑团队提交 Claim
→ 反例团队寻找最小失败实例
→ 另一个模型盲态重建证明
→ 形式化 Agent 固定定义和量词
→ 通过后进入公共 Claim 图
→ 下游归约团队才获得使用权限

如果后来发现反例，系统会自动标记所有下游证明，并提出资源回收建议。人类可以看到这次失败影响了哪些路线，以及其中是否留下了仍然成立的弱化版本。

这才是一套数学研究系统，而不是一群 Agent 轮流生成答案。

十、未来真正重要的，可能是“机器组织学”

我们习惯把 AI 能力理解为单个模型的能力：它能答对多少题、写多长的代码、完成多复杂的任务。

但当我们可以低成本调用大量模型以后，系统能力越来越取决于另一件事：

这些智能如何被组织起来？

同一个模型，放在不同制度里，可能产生完全不同的结果。

一个只奖励“尽快给出证明”的组织，会批量生产看起来漂亮的错误证明；一个要求独立攻击、保存失败和追踪依赖的组织，虽然更慢，却可能真正积累知识。

因此，未来的 AI 科研竞争未必只是“谁拥有最强的模型”，还可能包括：

• 谁拥有更好的研究任务分解制度
• 谁拥有更可靠的跨模型审查机制
• 谁能让失败结果成为长期资产
• 谁能把人类注意力放在最关键的争议上
• 谁能把成千上万次局部推理压缩成一条可信的知识链

60 个聪明 Agent 不会自动组成一个更聪明的整体，就像 60 个数学家也不会自动组成一流研究所。

模型提供智能，组织决定这些智能最终生产出噪音，还是知识。