科技资讯
一条模型厂商的科研公告，很容易被读成「AI 又赢了一次」。但对技术负责人、研发总监来说，值得抄进工作流的不是那三个结论，而是结论的交付方式：谁生成的、怎么验的、公开了什么、由谁复核。据 IT之家报道，OpenAI 宣布其模型在数学、计算机科学、物理学三个方向取得突破，并为此配套了 Lean 形式化验证、公开证明仓库、外部专家牵头审查等安排【1】。
下文不谈「AI 是否已经能做科学」，只谈三件和企业直接相关的事：工具边界、投入成本、合规口径。
图：示意图（AI 生成，非原文截图；模型 nano-banana-2）。仅作阅读辅助，事实以正文与参考文献为准。
一、真正变化的是速度：产出已经跑在人工审查前面
公告里有个不显眼但更值得记录的细节：数学方向，模型于 10 月 18 日生成证明，次日完成 Lean 形式化；计算机方向，10 月 16 日生成自然语言证明，17 日完成形式化，随后才启动外部合作机制【2】【3】。从「生成」到「机器可检验」，间隔以天计。
这意味着瓶颈位置变了。当 AI 能批量产出看起来完整、逻辑自洽的技术交付物时，团队的压力会从「写不出来」整体迁移到「验不过来」。这个迁移在软件团队里其实已经发生过一轮：代码补全普及之后，评审负担上升，测试覆盖率和静态检查成了主要的质量闸门。科研只是同一规律的极端样本——只不过那里的错误代价高得多。
所以，下面所有判断都围绕同一个问题展开：你怎么验收 AI 的产出。
二、三项成果不在同一可信度层级，最忌讳打包引用
把它们当成一条新闻的三个分句来传播，是最容易出错的读法。按证据等级拆开看，三者状态明显不同。
数学方向：已形式化，命题价值另论。 局部光滑猜想 1991 年由索格提出，用于描述波在聚焦时的行为；二维情形在 2019 年由古思、王虹、张睿翔解决，2025 年王虹与扎尔证明了三维挂谷猜想。此次模型给出的是所有维度下的证明，并由此推出挂谷猜想与斯坦因限制猜想【2】。模型撰写的自然语言证明与 Lean 形式化证明已上传公开代码仓库【2】。
计算机方向：已形式化，且引入了对抗式复核。 涉及的是指数时间假设（ETH），一个长期被当作布尔可满足性问题难度基准的猜想，数百篇论文以它为前提推导图论、计算生物学、数据库、计算几何等领域的难度结论【3】。OpenAI 邀请三位复杂性理论专家牵头验证与解释，并接受了两项条件：公开全部原始数据供独立验证、由公司出资举办学术会议讨论成果影响【3】。
物理方向：仍在审查中。 内容是在严格数学意义上证明四维空间中某些含规范场与费米子的相互作用量子场论确实存在，覆盖量子色动力学与标准模型的一种统一完备化，并顺带处理了纯杨–米尔斯理论存在性这一千禧年难题的子问题；审查由诺贝尔物理学奖得主大卫·格罗斯牵头的五人团队负责，尚未结束【2】。
把「已形式化验证」「已通过同行评议」「已获学界公认」当成同一件事，是这类报道传播中最常见的失真。企业对外引用时踩的坑，基本都出自这一步。
三、形式化验证的边界：它防推理错误，不防需求错误
Lean 这类证明助手能保证的，是从给定公理和定义出发，推理链可以被机器逐步检查通过。它不保证三件事：你证的命题是不是你真正想证的那个；这个命题本身有没有价值；建模时对现实的抽象是否站得住。
换成工程语言：CI 全绿，不等于需求写对了。形式化把「推理出错」的风险压到很低，同时把「问题定义错了」的风险原样保留，甚至放大——因为机器不会质疑前提。
按这个标准划线，场景适配度大致可以这么分：
- 值得考虑：结算与清分逻辑、智能合约、鉴权与权限模型、加密协议实现、并发调度器、事务隔离级别、嵌入式状态机。共同点是规则明确、状态空间可枚举、出错代价高。
- 不建议投入：规则高频变化的营销与推荐策略、需求还在探路的早期产品、连规格说明都写不出来的模块。在这些地方做形式化，产出通常是「证明了一个没人需要的命题」。
四、成本账：贵的不是工具，是把需求写成规格
形式化验证的显性成本不高，工具开源，学习资料充足。真正的开销在两头：一是把模糊的业务需求翻译成机器可检验的形式化规格，这一步通常占总投入的大头，且要求执行者同时懂业务与形式化方法；二是维护，需求一变，规格要同步改，否则验证结果立刻失去意义。
一个可操作的判断式是：错误代价 × 发生概率 > 规格撰写与长期维护成本。这个式子算不出精确数字，但能帮你在评审会上把「要不要做」变成「哪个模块先做」。
给预算有限团队的建议是做一个「反向 PoC」：不追求证出结论，只测一件事——把现有某个核心模块的规格写清楚，需要多少人天、卡在哪些地方。这个数据比任何演示都更能决定你未来两年要不要在这条线上投人。
五、合规三问：署名、数据、口径
第一问，署名归谁。 报道提到，合作团队邀请学术界共同讨论如何认定学术贡献等问题【3】。企业侧对应的现实麻烦是：AI 参与生成的专利交底书、算法方案、技术报告，发明人与作者怎么写？建议提前在内部制度里约定「AI 辅助产出」的标注规则，别等权属争议出现再补。
第二问，数据出不出得去。 把内部代码、模型结构、业务数据交给外部模型做审查或形式化，本质是第三方处理，可能触及数据出境。这类决定不适合由业务团队单独拍板，应走既有的数据分类分级与供应商评估流程。
第三问，对外怎么说。 在客户方案、融资材料、招聘宣传里引用前沿成果，务必带限定语。把尚未定论的研究当成产品能力背书，短期看起来有说服力，长期是合规与信誉的双重负债。比较稳妥的写法是：说明「该方向已有公开研究进展」，而不是「我们具备该能力」。
六、90 天可执行清单
- 第 1–2 周：在 AI 产出物的验收标准里加一条「可被机器检查」——测试、类型约束、形式化断言任选其一，替代纯人工过目。
- 第 3–6 周：选一个规则清晰的小模块做反向 PoC，只记录规格撰写的人力成本与卡点，不追求证明结果。
- 第 7–10 周：小范围复制外部对抗式复核结构。哪怕规模缩到一次内部评审：指定不看产出过程的独立评审人、开放原始材料、记录复核意见可追溯。
- 第 11–12 周：出两份内部文件——AI 辅助产出的署名与标注规则、对外引用前沿成果的表述口径清单。
七、接下来盯什么
三项成果最终是否站得住，要等学术界的独立确认。据公开报道，相关成果仍需进一步验证【1】。对企业的观察价值在于四个可跟踪的信号：物理方向的证明是否通过同行评议；已公开的 Lean 证明是否被第三方独立复现；是否出现基于新复杂度结论的具体算法改进；公开仓库是否出现修订记录。
最后回到工具视角。这三项成果的意义，不在于「AI 能证明猜想」这句话本身，而在于它展示了一套可复制的交付结构：AI 大量产出、机器先验一遍、人类专家对抗式复核、原始数据全公开。这套结构今天就可以被任何一家认真使用 AI 的公司借走，成本远低于自研模型。工具的价值从来不只在结论有多响，更在于你能不能验收它。
参考文献
【1】OpenAI 宣布斩获三项重大科学突破，涉及数学猜想、计算机算法及千禧年难题 — https://www.ithome.com/1/018/203.htm 【2】同上（编辑注：局部光滑猜想与挂谷猜想的来龙去脉、物理方向量子场论存在性证明的范围与五人审查团队构成、10 月 18 日生成与次日形式化的时间线，均基于该来源的二次解读与转述） 【3】同上（编辑注：指数时间假设的含义、三位复杂性理论专家牵头、公开全部原始数据与出资举办学术会议两项条件、以及生成与形式化的日期，引自该来源）
