证明可以机检之后：AI 原创数学结果、Lean 信任链与“命题是否忠实”这道新关卡（深度版）

一、背景：几个必要的概念

3-SAT 与 ETH。3-SAT 问题给出一个由若干子句组成的逻辑公式，每个子句是至多三个变量（或其否定）的“或”，子句之间用“且”连接，问是否存在一组真假赋值使所有子句成立。验证一个答案很容易，但已知算法求解所需时间随变量数 n 指数增长。据 Papex 转述 Anthropic 论文，此前的纪录是确定性算法约 1.328ⁿ、随机算法约 1.308ⁿ [3]。指数时间假设（ETH）由 Impagliazzo 与 Paturi 提出，断言存在某个固定常数 δ > 0，使得任何算法都不能在 2^(δn) 时间内解 3-SAT——也就是说，底数可以变小，但不可能跳出指数。大量“条件下界”结论都建立在 ETH 之上 [1][3]。

ETH 被反驳不等于 P = NP。反驳 ETH 意味着 3-SAT 可以在“次指数”时间内求解，例如 2^(n/√log n)，它远小于 2ⁿ，但仍远大于任何多项式。两家公司的论文都明确表示，结果不直接涉及 P 与 NP 问题，也不产生实用算法 [2][3]。

Lean 与“内核”。Lean 是一种交互式定理证明器。人或 AI 写出证明后，由一个很小的“内核”程序逐步检查每一步推理是否合法。内核小，意味着它更容易被审查和信任。证明还依赖于少数几条“公理”；Lean 的标准公理是命题外延（propext）、选择公理（Classical.choice）和商类型可靠性（Quot.sound）[2]。关于 Lean 类型论本身的可靠性，一项 10 月的理论工作进一步证明：二阶算术语言中的公式，在“ZFC + 无穷多个强不可达基数”中可证，当且仅当它作为 Lean 中的类型可以被构造 [11]——这为“Lean 证明了什么”提供了更精细的数学刻画。

技术脉络：从“机器复核人类证明”到“机器提出新结论”

“AI 做数学”并不是 10 月才开始的故事。把几条线索串起来，可以看到三个阶段的跃迁。

第一阶段：形式化作为“复核工具”。以有限单群分类为例，据 Axiom 的回顾：1963 年 Feit 与 Thompson 证明“非交换有限单群的阶必为偶数”，论文长达 255 页、占满《太平洋数学杂志》一整期；1983 年 Gorenstein 宣布分类完成；遗留的“拟薄群”缺口直到 2004 年才由 Aschbacher 与 Smith 以 1,221 页的专著补上 [4]。而在形式化一侧，2012 年 Gonthier 领导的团队历时六年，在 Coq（现名 Rocq）中完成了 Feit–Thompson 定理的形式化，这被视为“如此深度的证明可以被完整机检”的早期示范 [4]。这一阶段的特点是：人类先写出证明，机器花数年时间去复核。

第二阶段：AI 进入“解题”与“填证明”。竞赛级定理证明基准逐步被攻克，本文讨论的 Maestro 在 PutnamBench 上已证明 672 题中的 669 题 [7]。基准接近饱和，促使研究者转向更难、更不易泄漏的评测，例如从本科生科研项目中收集开放问题的 ReuF2F [12]。与此同时，形式化工具开始围绕“人监督智能体”重新设计：Numina Fuse 的作者在三维 Kakeya 猜想的形式化中使用了该系统 [8]，而三维 Kakeya 猜想本身是 Wang 与 Zahl 在 2025 年证明的 [1]。

第三阶段（2026 年 10 月）：AI 产出新结论，形式化成为发布门槛。OpenAI 在 10 月 6 日已经按“直接公开 AI 输出”的方式发布过一次结果，10 月 26 日的三项结果沿用并扩展了这一做法 [1]。局部光滑猜想此前只在二维情形下由 Guth、Wang 与 Zhang 于 2019 年证明，这次 OpenAI 称模型给出了所有维数下的证明 [1]。Axiom 的 CFSG 项目则把“复核”推到了全新规模：它在已有 Lean 工作的基础上推进，其中纳入了约 120 万行来自 Qiuzhen-CFSG 的代码，最终在 24 天内完成整个分类定理的形式化 [4]。从“数年复核一个定理”到“数周形式化一个定理体系”，再到“模型先提出结论、随即附上 Lean 证明”，瓶颈随之从“证明写不出来”转移到“写出来的命题是否忠实、谁来审查”。

二、发生了什么：事实梳理

OpenAI 的三项结果（2026-10-26）[1]：

• 数学：模型给出了 Sogge 1991 年提出的局部光滑猜想在所有维数下的证明，基于一个新的辅助偏微分方程；该猜想蕴含 Kakeya 猜想与 Stein 限制性猜想。OpenAI 称于 10 月 18 日得到输出，次日完成 Lean 形式化，并公开了自然语言稿与 Lean 证明。Papex 指出，论文本身对限制性猜想的表述更窄（“在猜想范围的内部”），是否覆盖所有形式需由专家判断 [3]。
• 计算机科学：OpenAI 称其系统于 10 月 16 日找到 ETH 的自然语言反驳，10 月 17 日完成 Lean 形式化。由 Impagliazzo、Paturi（加州大学圣地亚哥分校）与 Williams（MIT）牵头的小组组织公开审查。三位审查人在公开信中写道：“我们的参与不应被视为对该结论的认证。”[3]
• 物理：模型于 9 月 9 日与 9 月 18 日分别产出纯 Yang–Mills 存在性与 QCD 存在性的自然语言证明，10 月 16 日完成 Yang–Mills 存在性的 Lean 形式化；由 Gross 牵头的小组负责后续，暂不公开 AI 产出的材料。Papex 强调，这一结果涉及存在性，并未涉及千禧年问题中的“质量间隙”部分 [3]。

OpenAI 同时提出了外部合作的四项原则——透明、不寻求学术署名、承认整理者的贡献、独立——并提到其对 Simons 基金会 500 万美元的资助 [1]。

Anthropic 的 ETH 反驳（2026-10-27 UTC）[2]：仓库说明称，一个确定性算法可在 2^o(n) 时间内求解 3-SAT；事实上它能以 2^O(n·log log n/√log n) 的时间统计 3-SAT 的满足赋值个数（#3-SAT）。仓库明确写道：“该结果纯粹是渐近的，对实际求解公式不说明任何问题。”据 Papex，Anthropic 论文称核心算法由内部 Claude 研究模型在 10 月 16 日找到，“1,400 万输出词元，无人工输入”，并称两项结果是“独立且同时”得到的；此外，论文估计实际收益“除非 n > 10⁷”否则不太可能显现 [3]。两家的论文给出相同的指数主项；OpenAI 的 Lean 范围说明则注明，其形式化证明给出的是较弱的指数 n(log log n)²/√log n [3]。

Axiom 的 CFSG 形式化（2026-10-26）[4]：有限单群分类定理被认为是人类写过的最长数学证明，原始证明约 15,000 页、500 余篇论文、约 100 位数学家。Axiom 称，团队于 10 月 1 日启动，以已有的 Lean 工作和内部“证明地图”为基础，把项目划分为 108 个里程碑、约 380 个小任务；数十个 AI 智能体在 24 天内产出约 4,310 万行 Lean 代码；10 月 10 日证明了魔群（Monster）是单群。形式化过程中发现了 34 处“值得注意的偏差”，其中最重要的一处与“非平衡群定理”（UGT）相关：智能体在 Walter 1986 年的证明中找到了一个闭包断言的显式反例，团队随后改写了证明路线。另一例来自 Aschbacher 与 Smith 的“拟薄群”卷：一条引理断言两个量相等，智能体用 SL₂(5) 找到反例（一个量为 1，而等式要求为 2），将等式改为不等式并补全了受影响的论证。参与咨询的原始工作者包括 Lyons 与 Solomon。

Axiom 的工程细节同样值得关注 [4]。首先是“假设蔓延”问题：早期一些看似可控的里程碑，实际依赖于大量未被证明的前提，智能体默认它们成立；团队因此删除了数万行建立在这些假设之上的代码，按更稳妥的计划重启了部分工作。其次是构建瓶颈：智能体产出证明的速度超过了 Lean 重新检查的速度，修改一个共享结果会迫使所有依赖它的结果重新检查；团队开发了在多台机器之间分发构建缓存、并行独立检查的系统，并把昂贵的有限计算外置为可单独检查的“证书”，使验证速度提升了数个数量级。第三是重规划：10 月 13 日只关闭了一个里程碑，团队专门组织智能体把未完成的里程碑拆成更小、表述精确的定理，并要求每个拆分方案说明这些小定理如何通过一个简短的 Lean 证明合成原里程碑。这三点——假设管理、增量验证、可追溯的任务拆分——对任何大规模智能体协作项目都有借鉴意义。

发布方式之争。OpenAI 对三项结果采用了三种不同的发布策略：数学结果直接公开 AI 输出；计算机科学结果公开输出并组建外部小组审查；物理结果由外部小组决定何时公开 [1]。Anthropic 则采用第四种路线：论文与 Lean 证明直接发布在自家 GitHub，并在 Hexagon 数学预印本库存档，声明“主要由 AI 生成”“部分内容经人类检查和理解” [3]。据 Papex 梳理，设于普林斯顿高等研究院的“数学与人工智能咨询组”（AGMAI）对“由公司指定数学家作为发布把关人”的做法提出了五点担忧——访问延迟或不平等、剥夺其他研究者的参与、选择偏差、借用声誉、并无必要——并呼吁 OpenAI 尽快公开 Yang–Mills 相关的自然语言与 Lean 产出；AGMAI 此前还建议，AI 产出应存放在不受发布方控制、有可引用标识、能记录修改的学术存储库中，并附带模型名称、提示、思维链、尝试次数、算力与成本等信息 [3]。这场争论的实质，是 AI 科研成果的“出处记录”应当由谁来保存、保存到什么粒度。

三、算法拆解 ①：“次指数”到底有多快？

一句话直觉：2^o(n) 的意思是“指数里的系数会随 n 增大而趋于 0”，但趋于 0 的速度可能极慢，以至于在任何现实规模下都与 2ⁿ 相差无几。

生活类比：一个“每年都在降价”的商品，如果每年只便宜万分之一，理论上终会变得很便宜，但在你的有生之年几乎感觉不到。

逐步拆解：

1. 传统纪录：时间约为 cⁿ（c ≈ 1.3），即 2^(n·log₂c)，指数系数是常数 log₂1.3 ≈ 0.38。
2. ETH 断言：存在常数 δ > 0，任何算法都至少需要 2^(δn)。
3. 新结果：时间为 2^(C·n·log log n/√log n)，指数系数 C·log log n/√log n 随 n 增大趋于 0，因此对任何固定的 δ，n 足够大后都会小于 δ——ETH 不成立。

关键公式：

T(n) = 2^( C · n · f(n) ),   f(n) = log log n / √(log n)
当 n → ∞ 时 f(n) → 0  ⇒  对任意 δ > 0，终有 C·f(n) < δ

• n：变量个数；T(n)：运行时间上界；C：一个未具体给出的常数（大 O 记号中的常数）。
• f(n)：指数中随 n 变化的系数；它趋于 0，但非常缓慢。

小算例（示意，取以 2 为底的对数，忽略常数 C）：

• n = 10⁶：log₂n ≈ 19.9，√log₂n ≈ 4.46，log₂log₂n ≈ 4.32，f(n) ≈ 0.97。
• n = 10¹²：log₂n ≈ 39.9，√ ≈ 6.32，log₂log₂n ≈ 5.32，f(n) ≈ 0.84。

也就是说，即便在万亿级变量规模下，指数系数仍接近 1，再乘上未知常数 C，很可能不如现有的 1.3ⁿ 级算法。这与 Anthropic 论文“除非 n > 10⁷ 否则不太可能显现收益”的判断方向一致 [3]，也解释了两家为何都强调“纯理论意义”。

为什么重要、何时“失效”：它的意义在于理论版图——数百篇以 ETH 为前提的条件下界失去了依据，SETH 等更强假设随之失效（据 Papex 转述 OpenAI 论文 [3]）；但部分下界可由更弱、可能仍然成立的假设推出。它对工程实践的直接影响接近于零，任何声称“AI 让 SAT 求解变快”的解读都是误读。

四、算法拆解 ②：Lean 信任链——一个证明被“相信”需要过几道关

一句话直觉：“Lean 验证通过”不是一个单点事实，而是一条链：命题文件是否忠实、证明是否被内核接受、用了哪些公理、换一个独立内核是否仍然通过。

生活类比：一份合同的可信，不仅要“签字盖章齐全”（内核检查），还要“条款写的就是双方谈好的内容”（命题忠实），“没有附加隐藏条款”（公理清单），以及“另一家律所复核也无异议”（独立内核）。

逐步流程（以 Anthropic 的 eth 项目为例 [2]）：

1. 短小的命题文件：MainResults.lean 只陈述“ETH 为假”和主定理，不含证明、只依赖 Mathlib。仓库明确写道：Lean 检查证明，但没有机器检查这个文件是否与论文说的一致，因此文件刻意保持简短，便于人类读者核对；论文附录列出了 Lean 表述与印刷表述的差异。
2. 构建与内核检查：固定 Lean 与 Mathlib 版本（v4.33.1），完整构建约 8 分钟（24 个虚拟 CPU，最大进程约 7 GB 内存）。
3. 公理审计：打印两条主结果依赖的公理，应只有 propext、Classical.choice、Quot.sound 三条标准公理。
4. 命题比对：用 Comparator 工具把被证明的定理与一个“挑战文件”中的命题逐一比对，防止“证明了一个被悄悄改过的命题”。
5. 独立内核复核：用另一个独立实现的内核 nanoda 重新检查证明，降低单一内核存在缺陷的风险。

伪代码：

trust(project):
assert human_review(Statement.lean ≡ paper_claims)     # 唯一不能自动化的一步
assert lean_kernel_check(project) == OK
assert axioms(main_theorems) ⊆ {propext, Classical.choice, Quot.sound}
assert comparator(Statement.lean, Challenge.lean) == match
assert independent_kernel_check(project) == OK          # 如 nanoda
return "形式上可信；语义忠实性依赖第一步的人工判断"

• human_review：人工核对形式化命题与论文命题是否一致。
• axioms(...)：证明所依赖的公理集合；出现 sorry（未完成证明的占位）或自定义公理即为不合格。
• comparator：确认被证明的定理与事先给定的命题完全一致。

小算例：若某项目在主定理里悄悄加入了一个额外假设“n ≥ 10¹⁰⁰”，内核检查、公理审计、独立内核都会通过，只有第一步“命题文件是否等价于论文”能发现问题。MechAlign 的一个案例正是如此：它在一个双曲群相关结果中，通过依赖检查定位到相对原稿缺失的一个维数约束（与上游声明的形式化范围一致）[6]。

为什么有效、何时失效：机器检查把“证明是否正确”的不确定性降到很低，但把全部剩余风险集中到了“命题是否忠实”上。Axiom 的经验也说明了这一点：其团队反复遇到“加一个假设是推迟了工作，还是改变了定理的含义”这一判断难题，审查必须比对“已证命题”与“目标命题”[4]。

五、算法拆解 ③：SemantEq——如何判断两个形式化命题“真正等价”

一句话直觉：检验一个形式化命题 P 是否忠实，常见做法是证明它与可信参考命题 Q 等价（P ↔ Q）。但如果 P 和 Q 都能被库证明为真，P ↔ True ↔ Q 就会“平凡成立”，证明器越强，越多不相关的命题对会被误判为等价 [5]。

生活类比：判断两份译文是否表达同一个意思，不能用“两份都是真话”来论证——“地球是圆的”和“水在 100 度沸腾”都是真话，但它们不是同一句话的译文。

逐步流程（2026-10-23）：

1. 不再只要求“存在 P ↔ Q 的证明”，而是要求 P 能只经过一系列允许的步骤变换为 Q，例如逻辑重排、用库中自身的等式改写。
2. 判断依据是 Lean 实际检查的证明项（proof term），而不是表面的策略脚本，防止“绕路”。
3. 提供无模型的搜索器 SemantEq-Eval 和面向审计的 ProofAudit。

关键公式：

平凡等价：⊢ P 且 ⊢ Q  ⇒  ⊢ P ↔ Q        （与内容无关，必须排除）
SemantEq：P = S₀ → S₁ → … → S_k = Q，每一步 S_i → S_{i+1} ∈ 允许步骤集合 A

• ⊢ P：P 在库中可证；S_i：中间命题；A：允许的变换集合（逻辑重排、库内等式改写等）。

小算例（示意）：P 为“对所有自然数 n，n + 0 = n”，Q 为“2 是素数”。二者在库中都可证，因此 P ↔Q 平凡成立，但它们显然不是同一陈述的两种写法——SemantEq 要求的变换链不存在，判为不等价。反过来，P′ 为“∀x, ¬(x > 3)”，Q′ 为“∀x, x ≤ 3”，只需用库中“非大于即小于等于”这条等式改写一步即可互变，判为等价。

结果（据论文数据）：在 ProofNetVerif 测试集（作者裁定标签）上，SemantEq-Eval 达到 100% 精确率、65.6% 召回，基线 BEq+ 为 95.8% 与 61.8%，代价是 CPU 时间增加 8.9 倍；ProofAudit 对 104 对非等价命题一个都没有误判为等价，并将召回从 65.4% 提升到 81.1% [5]。

为什么有效、何时失效：它把“等价”从“逻辑上互推”收紧为“结构上互变”，牺牲部分召回换取零误报。失效之处在于：需要一个可信的参考命题，而对全新的研究结果，往往并不存在这样的参考；这时就需要 MechAlign 这类项目级审查 [6]——它从 173 个 OpenAI Math 项目中审查了 201 个主结果，并构建了 501 个“论断—命题—上下文”三元组的 LeanReviewBench。

六、算法拆解 ④：Maestro——失败时“说清原因”，由全局协调者决定怎么办

一句话直觉：传统的分治式证明器遇到证不出的引理，只会继续拆分；但引理证不出可能是因为提示不够、引理本身是假的、或上层拆分方向错了。Maestro 让证明者报告“为什么失败”，由看得见全局的协调者选择对策 [7]。

生活类比：项目经理不能只听到“这块做不完”，而要知道是“缺资料”“需求本身有矛盾”还是“方案从一开始就走错了”，对策完全不同。

逐步流程（2026-10-19）：

1. 协调者把目标定理拆成证明树，分发给多个局部证明者。
2. 每个局部证明者只能修改自己的证明文件，不得添加 axiom 等声明；无法完成时，返回结构化的失败诊断与数学证据。
3. 协调者根据诊断选择对策：指导（给卡住的证明者更多提示）、纠正（发现引理为假，修改命题）、撤回重规划（整棵子树方向错误，回退并重新拆分）。
4. 在代码合成中，经检查的反例会把代码送回修复。

伪代码：

while not proved(root) and budget > 0:
for node in open_leaves(tree):
result = prover(node)               # 返回 成功 / 失败诊断
if result.failed:
match diagnose(result):
"缺乏指导" -> guide(node, hints)
"引理为假" -> correct_statement(node)
"拆分有误" -> retract(subtree(node)); replan(parent(node))

小算例（示意）：要证 A，计划拆为引理 B 和 C。C 反复失败，证明者报告“找到反例：当 x = 0 时 C 不成立”。传统系统会继续把 C 拆成 C1、C2，徒耗预算；Maestro 的协调者判断“引理为假”，把 C 改为“x ≠ 0 时成立”，并补一条处理 x = 0 的引理 D。

结果（据论文数据）：在 arXivLean 上证明 34/48，对比基线 19；PutnamBench 669/672；Lean-IMO 59/60；IMO 2026 题目 6/6 [7]。

为什么有效、何时失效：它把“失败”变成了信息，避免在错误方向上耗尽预算。其局限是协调者本身的判断可能出错，把“难但为真”的引理误判为假并修改命题——这又回到了命题忠实性问题，需要人工把关。

七、从工具到工作流：人在环路中的形式化

几项工作展示了形式化正在从“证明器”演变为“工作流”：

• Numina Fuse（2026-10-24）[8]：一个面向 Lean 4 的智能体原生应用。作者指出，Lean 代码可以通过编译却不表达预期的非形式含义，而且智能体写 Lean 的速度已超过人阅读的速度，因此系统围绕“人类监督智能体”设计，提供蓝图、依赖图与代码视图；论文报告了它在三维 Kakeya 猜想形式化中的使用。
• PaperFormalizer（2026-10-22）[9]：从论文的 LaTeX 源出发，把论文转写为陈述依赖图，逐条审查忠实性、歧义与正确性，再在 Lean 中形式化。凡是可能改变论文主张的决定，都交给作者本人。
• MechAlign（2026-10-26）[6]：针对“没有可信参考命题”的情形，它的抽取工具 LeanTrace 从已展开的声明中构建“陈述依赖图”：保留定义体和结构约束，排除证明体，并在显式的库边界处停止；审查模型据此判断主定理是否忠实表达了原稿论断，并给出带定位证据的差异报告。作者用它对 173 个 OpenAI Math 项目中的 201 个主结果做了初步审查，并用来自 OpenAI Math、费马大定理与 Kakeya 项目的材料构建了 LeanReviewBench。它的意义在于：命题忠实性必须放在整个项目的依赖中理解，主定理里的一个符号，其含义可能由几十个文件之外的定义决定。
• ReuF2F（2026-10-19）[12]：从本科生科研项目中收集 244 个形式化的开放问题，作为“未被广泛关注、不易泄漏”的留出评测；据论文数据，最好的模型约解决 40%。
• 可验证的程序优化（2026-10-20）[10]：让智能体在写出更快实现的同时，给出与原实现等价的机器检查证明——原实现本身就是规格，绕开了“写规格”这一瓶颈。据论文数据，在 Verina 的 189 个参考实现中，为 156 个产出了经证明的更快版本。
• 智能体算法设计（2026-10-26）[13]：智能体提出进化算法、用 Lean 守卫过滤有缺陷的设计、再证明期望运行时间上界，全程不做经验比较；据论文数据，使用前沿模型时，8 类问题上 15 次运行中有 12 次完成全流程并得到机器检查的期望运行时间上界；两款开放权重模型未能完成全流程。

八、横向对比

九、我们的观点

第一，“可机检”正在成为 AI 科学成果的入场券，但不是终点。OpenAI、Anthropic、Axiom 都把 Lean 形式化作为发布的前提。然而 Anthropic 仓库的一句话说得最清楚：没有机器检查命题文件是否与论文一致 [2]。我们认为，未来一段时间，“命题忠实性审查”会成为与“同行评议”并列的新环节。

第二，发现、验证与解释正在分离为三种不同的贡献。Papex 的分析指出，模型给出论断，Lean 与专家完成验证，人类学者再把冗长证明变成可理解的知识，三者的作者、日期与证据各不相同 [3]。这对署名、时间戳与存档基础设施提出了新要求。

第三，形式化的价值不只在“证明新定理”，也在“审计旧知识”。CFSG 形式化发现了 34 处值得注意的偏差 [4]，其中包括需要改写证明路线的反例。这提示我们，任何长期依赖“专家共识”的复杂知识体系，都可能藏着未被发现的缺口。

第四，对“AI 突破”的传播要保持克制。ETH 反驳在理论上意义重大，在工程上几乎没有直接影响；Yang–Mills 结果涉及存在性而非质量间隙。准确地复述“证明了什么、没有证明什么”，是科技传播的基本责任。

十、未来展望

6–12 个月：

• ETH 结果的公开审查将给出初步结论；无论结果如何，审查流程本身会成为 AI 科学成果发布的参考范式。
• 命题忠实性工具（如 SemantEq、MechAlign）与人在环路的形式化工作流（如 Fuse、PaperFormalizer）会被更多数学期刊和会议采用为投稿辅助。
• 更多“已知但冗长”的定理会被完整形式化，附带勘误清单。

1–3 年：

• 形式化验证可能从数学扩展到更多“有规格可依”的领域：算法正确性、程序优化等价性 [10]、协议与合约逻辑。
• 科研出版可能出现“三件套”标准：自然语言稿 + 形式化证明 + 命题对齐报告，并附带独立时间戳与模型使用记录。
• 风险在于“验证鸿沟”：AI 产出速度远超人类审查速度，若命题审查跟不上，形式化可能制造一种“看似已验证”的错觉。

十一、对金融风控与企业落地的启示

1. 把“命题忠实性”思想用到规则与模型验证上。风控规则、额度策略在系统里的实现，与政策文件中的表述是否一致，本质上就是“命题是否忠实”的问题。可以借鉴 Anthropic 的做法：把核心规则写成短小、可人工核对的“规格文件”，再验证实现与规格一致。
2. 在关键计算上引入可验证的等价性检查。对风险计量、定价、额度计算等模块的性能优化，可以参考“可验证优化”的思路 [10]：优化后的实现必须与原实现等价，而不只是通过测试。
3. 建立“失败原因”报告机制。Maestro 的经验对模型开发同样适用：模型效果不达标时，要区分“数据不足”“假设错误”“方案方向错误”，对策各不相同。
4. 审慎对待“AI 突破”类信息。在制定技术路线时，应区分理论进展与工程可用性。

弘犀智能在规则引擎与评分卡建设中始终强调“规格清晰、实现可验、结论可解释”。形式化方法在数学界的这次集中亮相，进一步印证了这一方向的价值。

十二、结语

10 月下旬的这几件事，标志着 AI 在数学领域从“解题”走向“交付可机检的研究成果”。但机器检查只回答了“证明是否正确”，“证明的是不是我们关心的命题”仍然需要人来回答。对科研界和企业来说，下一阶段的关键能力，是把“规格写清楚、让人看得懂、能被独立复核”做成制度。

想了解弘犀智能在规则治理与可解释风控方面的实践，欢迎点击文末「阅读原文」访问 www.hxallai.com。

参考文献

1. [1] OpenAI. Working with academic communities to build scientific understanding. OpenAI, 2026-10-26. https://openai.com/index/building-scientific-understanding-with-academic-communities
2. [2] Anthropic. anthropics/formal-math：eth 项目（A 2^o(n) Time Algorithm for 3-SAT，论文与 Lean 4 形式化）. GitHub, 2026-10-27. https://github.com/anthropics/formal-math
3. [3] Papex. OpenAI's Kakeya, ETH and Yang–Mills claims: what they say and what stays open. Papex Blog, 2026-10-27.（第三方解读）https://papex.org/blog/claimed-verified-explained
4. [4] Axiom. Formalizing the Enormous Theorem. Axiom Math, 2026-10-26. https://axiommath.ai/research/the-enormous-theorem-formalized/
5. [5] Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar et al. SemantEq: Faithful Bidirectional Equivalence of Formal Statements. arXiv, 2026-10-23. https://arxiv.org/abs/2610.32919
6. [6] Hao Shen, Ruichen Qiu, Lihong Zhi, Xiao-Shan Gao. MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization. arXiv, 2026-10-26. https://arxiv.org/abs/2610.35269
7. [7] Haoyu Li, Zeren Shui, Yuhao Zhang, Ferhat Erata et al. Maestro: Agentic Formal Proof Development by Coordination. arXiv, 2026-10-19. https://arxiv.org/abs/2610.25920
8. [8] Justin Asher, Yichuan Cao, Ruichen Qiu, Pietro Pellegrino et al. Numina Fuse: Interactive Autoformalization in Lean 4. Project Numina, 2026-10-24. https://arxiv.org/abs/2610.33860
9. [9] Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet. PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean. arXiv, 2026-10-22. https://arxiv.org/abs/2610.31810
10. [10] Zhe Ye, Udaya Ghai, Zhizhen Qin, Dawn Song et al. Agentic Verified Optimization of Real-World Software. arXiv, 2026-10-20. https://arxiv.org/abs/2610.30188
11. [11] Lorenzo Bresolin, Marcello Mamino. Reflections on Trusting Lean. arXiv, 2026-10-21. https://arxiv.org/abs/2610.30433
12. [12] Zeyu Zheng, Yiyang Liu, Yuyang Zhao, Congmin Zheng et al. ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems. arXiv, 2026-10-19. https://arxiv.org/abs/2610.27046
13. [13] Per Kristian Lehre. Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean. arXiv, 2026-10-26. https://arxiv.org/abs/2610.35595

弘犀研究 · 前沿 AI 深度综述 · 弘犀智能