摘要：Star Fleet Math把数学研究拆成多条并行线路，让多个智能体分别承担检索、探索、编程、形式化和验证任务。真正决定成果质量的，不只是模型数量，而是任务结构、验证工具和研究人员的判断。
一名研究人员面对20道数学难题，通常只能逐题阅读、查资料、尝试证明。
Star Fleet Math采用了另一种方式：在一台Mac桌面应用中同时启动最多20个数学智能体，每个智能体负责一道题，使用独立的GPT-5.6实例和一台60核服务器。遇到大规模枚举、组合搜索或计算实验时，系统还可以调用更多CPU和GPU资源。每个智能体拥有单独的工作目录、工具链、文献检索和长期记忆。
任务分配完成后，20条研究线路可以同时推进。
有的智能体检索已有定理，有的编写程序寻找反例，有的构造证明框架，有的把数学表达转换成Lean 4代码，还有独立的验证智能体检查提交结果。
这种工作方式接近一支由多名研究助理、程序员和证明审查员组成的研究团队。
区别在于，所有成员都是软件智能体，工作过程可以复制、暂停、回滚和重新分配。
一、单个AI为什么很难处理长期数学研究
数学研究需要保持较长的推理链。
一个开放问题可能涉及：
- 准确定义研究对象；
- 查找几十篇相关论文；
- 整理已知结论；
- 识别已有方法的限制；
- 提出多个证明方向；
- 编写计算程序；
- 搜索反例；
- 构造辅助引理；
- 检查各个引理之间的依赖；
- 整理完整证明；
- 核对最终命题是否和原问题一致。
单个大模型可以对其中某一步给出有价值的建议，却容易在长流程中出现上下文混乱。
常见问题包括：
- 前面使用的定义在后面发生变化；
- 某个辅助结论未经证明便被继续引用；
- 搜索失败后重复尝试相同路线；
- 局部推导正确，整体证明缺少关键环节；
- 修改一个引理后，没有同步检查后续依赖；
- 最后证明的命题与最初问题存在细微差异。
数学研究的困难往往集中在整体结构。
AI可能完成若干局部证明，却没有补上连接这些局部结果的全局步骤。2026年一项Lean形式化案例中，AI成功证明了四个辅助引理，但主定理仍保留一个未解决的证明占位符。缺失部分恰好是把局部结论组织成完整组合计数论证的关键步骤。
将所有工作放进一个连续对话，会让错误不断累积。
多智能体系统尝试把长任务拆开，让每个智能体只维护一段较小、边界明确的工作。
二、20个智能体并行，不等于让20个模型重复回答同一个问题
最简单的多模型方法，是把同一个问题发给20个模型，再从20份答案中选择一份。
这种方式可以增加答案多样性，但大量计算会浪费在重复工作上。
Star Fleet Math采用的是任务分工。
每个“星舰”智能体负责一个独立数学问题，拥有自己的服务器、记忆和工具。系统页面显示，其研究对象包括Erdős问题、FrontierMath问题和千禧年难题。项目把部分结果标为“拟议解答”，并同时提供Lean工程、证明报告和验证材料。
在单个问题内部，还可以继续拆分角色。
一套较完整的数学智能体系统通常包括以下几类角色。
1. 规划智能体
规划智能体先分析问题结构。
它负责：
- 提取定义和条件；
- 查找相关领域；
- 把目标拆成若干子目标；
- 确定子目标的先后关系；
- 分配计算、检索和证明任务；
- 记录尚未解决的环节。
2026年7月发布的开源系统OpenProver采用Planner、Worker和Verifier架构。Planner维护一块精简的工作白板和一个不受短上下文限制的中间结果仓库，再将工作分给多个并行Worker。
2. 检索智能体
检索智能体负责查找：
- 数学论文；
- 已有定理；
- Mathlib中的形式化引理；
- GitHub上的Lean工程；
- 相关算法；
- 反例和计算记录。
Star Fleet Math建立了Lean 4定理和引理检索库，并索引arXiv论文与GitHub仓库。智能体可以用自然语言搜索已有形式化结论，减少重复证明。
3. 探索智能体
探索智能体尝试不同证明方向。
同一道题可以分配多条路线：
- 归纳法；
- 反证法；
- 概率方法；
- 极值方法；
- 代数转换；
- 图论构造；
- 计算机枚举；
- SAT或SMT求解；
- 寻找反例。
这些智能体互不覆盖工作区。
其中一条路线失败，不会破坏其他路线的中间结果。
4. 程序智能体
很多数学问题需要计算实验。
程序智能体可以编写Python、Rust、C++或CUDA代码，用于：
- 枚举有限情况；
- 验证猜想；
- 搜索反例；
- 测试参数范围；
- 计算数值结果；
- 建立组合结构；
- 调用计算机代数系统；
- 将大型搜索拆成多个独立任务。
Star Fleet Math为每个智能体提供SAT、SMT、约束规划和计算机代数工具，包括Z3、SageMath、PARI/GP、GAP和Macaulay2等。
5. 形式化智能体
形式化智能体把自然语言证明写成Lean 4代码。
Lean是一种开源编程语言和证明助手。数学命题需要被写成精确的形式化定义，证明中的每一步都要通过Lean内核检查。
自然语言中的“显然”“容易得到”“类似可证”，在Lean中通常需要展开成具体步骤。
形式化智能体因此会暴露许多人类论文中被省略的细节。
6. 验证智能体
验证智能体检查：
- 代码能否编译；
- 是否存在未完成的证明占位符；
- 使用了哪些公理；
- 定理陈述是否符合原问题；
- 辅助引理是否存在循环依赖；
- 证明是否依赖未授权的假设；
- 计算结果能否重复。
Star Fleet Math还设置了单独的证明审查工具，系统通过后可以再请求人工复核。
三、Lean 4为什么成为这类系统的重要工具
大模型生成一段数学证明时，语言可以很流畅。
其中仍可能隐藏几类错误：
- 漏掉特殊情况；
- 使用并不存在的定理；
- 混淆充分条件和必要条件；
- 把数值实验当成一般性证明；
- 在推导中改变变量范围；
- 引入未经说明的假设；
- 证明了一个更弱或不同的命题。
仅靠另一个大模型阅读，很难把这些错误全部找出来。
Lean 4采用形式化验证。
研究人员需要先用精确语言描述：
- 对象是什么；
- 变量属于什么集合；
- 假设有哪些；
- 结论是什么；
- 每一步用了哪个定义或定理。
Lean的内核只接受能够从现有公理、定义和已验证引理中推导出的证明。官方将其定位为可用于形式化数学以及软硬件验证的证明助手。
因此，Lean更像一台严格的证明编译器。
代码通过编译，说明形式化命题在给定逻辑体系中得到了证明。
但这里仍有一个重要边界：
Lean验证的是写进系统的形式化命题，不会自动判断这条命题是否准确表达了人们最初提出的问题。
如果智能体在形式化阶段缩小了变量范围、增加了额外条件，或者换成一个较弱命题，Lean仍然可能顺利验证。
所以数学智能体系统需要两种审查：
- 证明代码是否正确；
- 形式化命题是否忠实对应原问题。
第一项可以交给Lean内核。
第二项仍需要熟悉该领域的数学家检查。
四、共享工作白板解决什么问题
多智能体系统容易出现另一类麻烦：每个智能体都有自己的结论，却无法拼成一份一致的成果。
例如：
- A智能体使用定义一；
- B智能体使用定义二；
- C智能体引用A的旧版本；
- D智能体证明的引理没有记录适用条件；
- E智能体修改了符号，但没有通知其他成员。
研究团队需要一个共享的系统记录。
LeanMarathon提出了“演化蓝图”方法：使用一份Lean文件同时保存形式化证明骨架、自然语言证明关系和任务状态。四类智能体分别负责构建、审查、证明和修复，各自只能修改合同规定的部分。系统先稳定目标命题，再按照证明依赖图，从底层引理向上并行推进。
这种蓝图可以记录：
1 | 主定理 |
每个智能体只处理一个节点。
节点通过验证后，再进入上层证明。
如果某个节点失败，系统重新分配这个局部任务，无需从头启动整项研究。
LeanMarathon在两篇研究论文涉及的四个Erdős问题上进行测试，三次自主运行完成了七个目标定理的形式化，共证明258个引理和定理，最终文件不含未解决的sorry占位符。
这个结果说明，长期科研任务需要稳定的工程结构。
模型能力仍然重要，任务图、版本控制、局部权限、持续验证和失败恢复同样重要。
五、为什么要把规划、证明和验证分开
让同一个智能体提出猜想、完成证明，再自行判断证明是否正确，容易产生确认偏差。
它已经沿着某条路线投入了大量计算，后续审查时可能继续接受这条路线中的隐含假设。
角色分离可以降低这种风险。
例如：
- Planner只负责拆解任务，不直接宣布证明完成；
- Builder负责构造证明；
- Verifier只接受能够通过Lean的结果；
- Critic专门寻找反例和定义偏差；
- Human Reviewer检查问题表述和数学价值。
LAMP系统采用Planner、Builder和Verifier分工，并通过MCP向智能体提供特定数学领域的结构化知识。在90个“词组合数学”定理测试中，系统生成了87个通过Lean内核验证的证明，成功率为96.7%。研究中的消融实验显示，移除工具支撑架构或者取消Planner与Builder的分工，成功率都会下降约12个百分点。
这个结果可以作出一个工程判断：
多智能体系统的价值，部分来自模型数量，更多来自角色边界和验证流程。
如果20个智能体拥有完全相同的任务、提示词和工具，它们可能重复产生类似结果。
明确分工后，计算资源才会覆盖更多研究方向。
六、长期记忆怎样帮助证明不断积累
一个数学项目可能持续数周或数月。
智能体每次重新启动后，需要知道：
- 哪些路线已经失败；
- 哪些定理已经验证；
- 哪些代码可以复用；
- 哪些引理依赖特定版本；
- 哪些搜索参数已经测试；
- 哪些反例推翻了旧猜想；
- 哪些结果得到人工认可。
普通对话记录很难承担这种工作。
对话中包含大量尝试、错误、解释和临时信息。全部重新放进上下文，会占用大量Token，也容易让模型引用过期内容。
Star Fleet Math使用长期记忆系统，将通过验证的Lean定理和引理组织成依赖图。后续智能体可以搜索这些结果，并在已有证明上继续构建。
较可靠的科研记忆应区分几种状态：
- 未验证猜想；
- 计算实验支持的结论；
- 已通过Lean验证的引理；
- 已由人工审查的定理；
- 已失败的方法；
- 仅在特定条件下成立的结果。
如果把所有内容都当成同等可靠的知识，错误会进入后续任务。
长期记忆系统需要保留来源、验证状态、适用条件和版本信息。
七、并行智能体也会带来大量成本
20个智能体同时运行，需要20份模型推理资源、20套执行环境和大量工具调用。
如果每个智能体都拥有60个虚拟CPU，仅基础服务器配置便达到1200个虚拟CPU。大规模搜索还可能调用数千个CPU核心或H100 GPU。
成本不仅来自模型Token。
还包括：
- 云服务器；
- GPU计算；
- 文献索引；
- 向量数据库；
- 代码执行环境；
- 形式化编译；
- 中间文件存储；
- 失败任务重试；
- 人工审核；
- 安全隔离。
并行数量越多，重复探索也可能越多。
因此，调度器需要判断：
- 哪个问题值得分配更多计算；
- 哪条路线已经表现出失败迹象；
- 哪些智能体应当提前停止；
- 哪些中间结果可以共享；
- 哪些任务可以使用较小模型；
- 哪些环节需要高推理模型；
- 哪些步骤适合确定性程序。
简单的信息提取和格式转换，没有必要占用最强模型。
困难的证明规划、反例分析和跨领域推理，可以使用更高成本的模型。
资源调度本身会成为科研智能体系统的一项核心能力。
八、20个智能体给出的“解答”能否直接发表
不能只看页面上写了多少个“已解决问题”。
一项开放数学问题的确认通常需要经过多层检查：
第一层：形式化代码能否通过
Lean项目需要完整编译，不能包含未解决的sorry或其他证明占位符。
第二层：命题是否准确
数学家要检查Lean中的定义、变量范围和结论，确认它们与原问题一致。
第三层：是否使用了过强假设
部分证明可能在形式化时加入原问题没有给出的条件。
第四层：是否已有公开结果
一个被列为开放的问题，可能已有论文、预印本、部分解答或未被数据库及时收录的结果。
Star Fleet Math也在页面中说明，一些标为开放的问题可能已经存在非正式或部分答案，并承认归属判断可能出现错误。
第五层：证明是否具有数学价值
形式化证明可以非常长，依赖大规模计算或复杂自动化。
数学界还会关心：
- 是否给出了可理解的新方法；
- 是否揭示了问题结构；
- 是否可以推广；
- 是否能被同行复查；
- 是否适合写成正式论文。
第六层：独立复现
其他研究者需要在独立环境中构建Lean工程，核对依赖版本，并重复关键计算。
因此，“机器验证通过”和“数学界确认解决”之间还有一段审查过程。
九、这种模式能否用于工业研发
数学证明具有一个很大的优势：Lean可以给出明确的通过或失败结果。
工业研发中的很多任务没有这样的统一验证器。
一个智能体完成机械设计后，系统不能只检查CAD文件是否能打开。还要验证：
- 结构强度；
- 疲劳寿命；
- 制造可行性；
- 材料成本；
- 装配干涉；
- 安全标准；
- 现场工况；
- 供应链条件。
即便如此，多智能体并行方式仍可用于工业研发。
场景一：CAE仿真方案搜索
一个总体智能体接收设计目标后，把任务分给多个子智能体：
- 一个负责几何清理；
- 一个负责网格策略；
- 一个负责材料参数；
- 一个负责边界条件；
- 多个智能体测试不同求解参数；
- 一个智能体比较结果；
- 一个智能体检查仿真设置是否符合规范。
每条路线进入独立计算环境。
结果统一写入试验记录，再由工程师选择后续方案。
场景二：工艺参数优化
多个智能体可以分别探索：
- 温度组合；
- 压力组合；
- 进给速度；
- 刀具参数；
- 能耗约束；
- 质量指标；
- 设备负载。
实际执行前，参数需要通过工艺规则、仿真模型和人工审批。
场景三：故障原因分析
不同智能体分别从以下方向分析：
- 传感器趋势；
- 维修记录；
- 报警序列；
- 工艺变化；
- 环境因素；
- 同型号设备案例；
- 备件批次；
- 操作日志。
最后由审查智能体整理证据链，标出相互支持和相互冲突的结论。
场景四：工业软件中试验证
中试平台可以把一个工业软件测试任务拆成：
- 安装验证；
- 接口验证；
- 数据兼容性验证；
- 多工况计算；
- 参数组合测试；
- 性能测试；
- 异常恢复测试；
- 结果一致性检查；
- 报告生成。
多个智能体同时运行不同测试用例，确定性测试程序负责判定结果，人工负责解释异常和确认业务有效性。
场景五：技术文献与专利分析
不同智能体分别负责：
- 专利检索；
- 论文检索；
- 技术路线分类；
- 权利要求对比；
- 关键参数提取；
- 竞争企业分析；
- 技术空白识别。
所有引用需要回到原始论文和专利文件核对。
十、工业科研需要自己的“Lean”
数学领域有Lean内核。
工业领域需要为不同任务建立相应的验证器。
例如：
- CAD模型使用几何规则和干涉检查；
- CAE结果使用收敛性、守恒关系和基准算例验证；
- 工艺方案使用工艺窗口和设备约束检查；
- 控制逻辑使用仿真器、数字孪生和安全联锁验证；
- 数据分析使用统计测试和历史数据回测；
- 软件代码使用编译器、单元测试和静态分析；
- 技术报告使用引用核查和数据一致性检查。
验证器越明确，智能体可以获得的自主权限越高。
缺少验证器时，智能体适合提出方案和整理材料，不适合直接作出高风险决策。
企业构建科研智能体系统时，可以先回答三个问题：
- 任务能否被拆成边界清晰的子任务；
- 每个子任务是否有可检查的输出；
- 系统是否存在独立于大模型的验证手段。
三个条件都具备，适合采用多智能体并行。
如果任务目标含糊、结果无法测量、错误代价很高，则需要增加人工控制。
十一、多智能体科研的核心是一套研究工程
20个大模型同时运行，画面很有冲击力。
系统能否持续产出可靠结果，取决于更多基础工作：
- 如何定义问题；
- 如何拆解任务；
- 如何分配资源；
- 如何隔离工作环境；
- 如何管理中间结果；
- 如何记录失败路线；
- 如何控制版本；
- 如何验证输出；
- 如何处理角色冲突；
- 如何把人工意见写回流程。
科研活动因此具有了更多软件工程特征。
研究计划可以表示成任务图，证明和实验可以进入版本库，每个结论可以附带来源和验证状态，失败任务可以重新调度，多个研究方向可以同时推进。
数学问题为这套方法提供了较清晰的试验场，因为证明结果能够交给Lean内核检查。
工业研发面对的数据更杂、约束更多、验证手段分散，需要把仿真软件、试验设备、行业标准、知识库和人工审查放进同一套流程。
单个模型负责回答问题。
多智能体科研系统负责组织一项工作：拆解、搜索、计算、验证、记录和复核。
20个智能体可以同时工作。
决定成果质量的，仍然是任务结构、验证工具和研究人员的判断。