费马大定理已经由安德鲁·怀尔斯在上世纪九十年代完成证明，但把这份跨越多个现代数学分支的成果完整翻译成机器能够逐步核验的语言，长期以来仍是一项以年计算的工程。如今，Anthropic披露的项目把这道门槛猛地向前推了一大步：Claude在十一天内协助完成端到端Lean形式化工作，最终形成约一千三百万行代码、三万零三百条可验证定理，其中约二万九千五百条进入最终证明。
这件事真正改变的不是费马大定理“是否成立”，而是复杂知识如何被审计。人类论文依赖专家阅读、背景知识与同行共识，Lean则要求每一步推导都能被内核重新编译。AI在这里不只是生成一段看似合理的答案，而是提交一份可以被独立工具拒绝或接受的证据。与GPT-6 Astra在开放数学问题基准中的表现放在一起看，前沿模型正在从会解题、会表达，走向必须为结论交付完整验证链。
一千三百万行证明
费马大定理的现代证明涉及椭圆曲线、模形式等大量前置理论，形式化并不是把怀尔斯的论文逐句输入电脑。每个定义、引理和依赖关系都要转写成Lean可理解的对象，缺失的数学基础还得先补齐。因此，项目产出的绝大部分代码都在搭建通往最终定理的基础设施，它更像修建一整套数学铁路网，而不是只铺最后一公里。
据项目公开信息，最终证明只依赖三条基础公理，并通过Lean编译器检查。这个“通过”很关键：语言模型可能写出语气自信却逻辑断裂的推导，但证明助手不会因为表述漂亮而放行。代码规模本身并不等于数学价值，能够由一个小型、明确的可信内核重新验证，才是成果最有分量的部分。
多智能体如何协作
几十个智能体并行并没有天然带来效率。早期尝试中，不同Agent难以同步进度，重复劳动、依赖缺失与上下文遗忘很快累积，最后被采用的代码占比很低。团队随后构建Prove2Me平台，用定理依赖图拆分任务，把“下一步该证明什么”变成可追踪的节点，并将定理陈述与证明实现分开管理。
这种工程组织方式比单次模型跑分更值得企业关注。长任务失败往往不是模型不会写某一段内容，而是它不知道已经完成了什么、还依赖什么、谁有权修改哪一部分。自然语言索引帮助Agent检索已有成果，依赖图避免下游建立在空缺节点之上，Lean编译则充当持续集成系统。数学项目由此呈现出与大型软件工程相似的结构：任务编排、版本状态、自动测试和最终验收缺一不可。
开放难题的受控测试
Epoch AI与曼彻斯特大学推出的FrontierMath Erdős基准，则把模型直接放进开放问题考场。该基准从Erdős问题库中选择六十八道仍未解决、彼此相对独立且具有研究价值的猜想，并要求模型提交Lean证明。标准测试中，每道题设置三百美元预算、七十二小时上限和一次尝试，验证容器与Agent工作容器相互隔离，最终代码需要在干净环境中重新编译。
GPT-6 Astra在标准条件下解出两道题，得分率约为百分之三，是参与测试的模型中唯一拿到非零成绩的一款。研究团队在放宽预算、调整Agent配置后的追加测试中累计得到五道问题的可验证结果，但这些追加成果不应与标准榜单成绩混为一谈。六十八道题仍有六十三道悬而未决，也说明“解出几题”距离自动化数学家还有很长距离。
成本也要被验证
这次测试把过去经常被忽略的失败次数、计算预算和人工介入程度摆到了台面上。五道开放问题的全部尝试累计花费超过二十二万美元，按基准条件估算，解出一道重要开放问题的期望成本约为一万美元。对于有望进入顶级期刊的数学成果，这个价格可能并不昂贵；但对普通研究任务而言，能否控制尝试次数和验证开销将直接决定产品是否可用。
更重要的是，形式化失败不一定代表数学思路完全错误。模型可能找到有价值的论证，却因为Mathlib缺少某项前置结果，或者无法把自然语言思路准确翻译成Lean而未能通过。未来评测需要同时记录研究洞察、形式化完成度、资源消耗和人类修订量，不能用一个总分抹平不同环节。AI科学的成本核算，也应从Token数量扩展到专家复核、实验设备和失败恢复。
走进物理实验室
数学中的“可编译证明”正在其他科学领域对应为“可复现实验”。Physical Superintelligence完成五千八百万美元种子轮融资，核心产品Emmy试图让虚拟物理学家自动拆解问题、运行仿真并根据结果继续推演，已探索数据中心优化和轨道测算等场景。资本看中的并非聊天界面，而是模型能否进入带有物理约束、成本约束与真实反馈的任务。
鼎犀智创的材料研发路线更接近完整闭环：AI Scientist提出方案，自主实验室负责样品制备、多模态表征和数据回流，再根据结果调整下一组实验。公开信息显示，其系统在万级参数空间中把原本预计约二千天的多目标寻优压缩至四天，并推动复合纤维进入中试。这里的关键不是“预测了多少候选材料”，而是预测能否被合成、测量并进入放大验证。
药物研发的证据链
Owkin与勃林格殷格翰达成许可合作，则展示了AI科学家进入制药流程的另一种方式。K Pro把多模态患者数据、生物模型和可复现分析放在统一环境中，研究人员可以用自然语言提出问题，再沿着数据来源和分析步骤检查结果。Owkin公布的内部数据称，药物靶点识别周期可从十二个月以上缩短至三个月。
医疗与生命科学不能把语言流畅度当作正确性。患者数据的使用范围、样本偏差、模型版本、分析参数和结论复现都需要记录，候选靶点也必须继续接受实验和临床验证。AI在这一领域最现实的角色，是缩小搜索空间、组织证据和加速迭代，而不是绕过科学流程直接宣布答案。
竞争转向可复核结果
从Lean证明、开放问题基准到材料与药物实验，这些进展共享同一条主线：模型的价值开始由“生成得多快”转向“结果能否被第三方复核”。数学依靠证明内核，软件依靠测试与版本控制，材料依靠仪器数据和重复实验，药物研发依靠多模态证据与临床链路。不同领域的验收工具不同，但都在压缩模型凭空自信的空间。
对研究机构和企业而言，下一步不应只是采购更强模型，而要先建设可验证的工作流：把任务拆成明确节点，保存数据与工具版本，为高风险动作设置人工审批，让失败结果也能进入知识库，并用独立环境重跑关键结论。模型能力还会继续上涨，真正稀缺的却可能是高质量数据、可靠验证器、实验自动化设备，以及能把机器输出转成可信成果的人。AI科学的分水岭，最终不会是一句更响亮的“突破”，而是一条别人可以重新走通的证据链。
