AI 形式化证明流水线：从自然语言论证到 Lean 内核核验-平芜编程栈

面向关注 AI for Science、数学软件和高可信推理的开发者，本文不讨论某个数学结论是否已经获得学界最终认可，而是借助 2026 年公开的 Navier–Stokes 解答与 Lean 形式化案例，解释“模型提出证明、机器核验形式证明”的工程链路。读完后你能区分自然语言论证、形式化证明和独立同行评审，并搭建小型验证工作流。

三种“正确”不能混为一谈

OpenAI 在 2026 年 9 月公开称，其内部系统给出了 Navier–Stokes 存在性与光滑性问题的一个解答，并同时提供论文式说明与 Lean 形式化证明。面对这类重大声明，工程人员最容易犯的错误，是把“模型生成了证明”“Lean 接受了代码”和“数学共同体确认了结论”当成同一件事。

自然语言证明负责传达思想，但可能省略条件。形式证明把定义、假设和推导编码为可由小型内核检查的证明项，能排除大量逻辑跳步。同行评审则要判断形式化问题是否与原命题一致、定义是否偷偷改变，以及论证是否具有数学价值。三层互相支持，却不能互相替代。

Lean 内核到底核验什么

Lean 建立在依赖类型理论之上。直观地说，一个命题被表示为类型，证明是该类型的一个值。策略、自动化和 AI 可以帮助构造这个值，但最终输出仍由可信内核检查。Lean 官方教材指出，许多高层命令会被编译为更基础的证明项；即便自动化工具本身不在可信计算基中，其产物也必须通过内核。

theorem add_zero_demo (n : Nat) : n + 0 = n := by induction n with | zero => rfl | succ k ih => simp [ih]

这个小例子使用归纳法证明自然数加零不变。induction与simp帮助生成证明，但检查结果并不依赖读者相信这些策略“聪明”。真正关键的是所有未解决目标都被关闭，而且没有引入超出项目允许范围的公理。

从论文到形式化的四层流水线

第一层是命题对齐：将论文中的对象、量词、边界条件和正则性假设逐项映射为形式定义。第二层是引理图谱：把长论证拆成具有明确输入输出的小引理。第三层是证明生成：人类、搜索程序或语言模型提出策略与中间项。第四层是内核验证与审计：检查编译结果、依赖、公理、版本和可复现环境。

自然语言命题 ↓ 逐项对齐审计 形式定义 → 引理依赖图 → AI/人工构造证明项 ↓ Lean 内核检查 ↓ 可复现构建 + 外部数学评审

“逐项对齐审计”是最不能省略的一步。一个形式证明可能完全正确，却只证明了原问题的弱化版本。例如把“所有平滑初值”不小心换成某个特殊初值，内核不会替你发现研究问题被改写，因为它只检查给定形式命题。

给 AI 的任务要可验证

不要直接让模型“证明整个定理”。更可靠的接口是提供当前目标、可用引理、禁止使用的公理、时间预算和期望输出格式。模型返回 Lean 代码后，构建系统在隔离环境编译；失败信息被结构化反馈，但不能让模型执行任意系统命令。

defproof_job(goal,allowed_lemmas,attempt):return{"goal":goal,"allowed_lemmas":sorted(allowed_lemmas),"attempt":attempt,"limits":{"seconds":30,"memory_mb":2048},"forbidden":["sorry","admit","new_axiom"],}defaccept(result):return(result.exit_code==0andresult.unsolved_goals==0andnotresult.forbidden_tokensandresult.axioms<=result.project_allowlist)

代码是独立的工作流示意。真实系统还要锁定 Lean 与 mathlib 版本、限制网络、记录编译日志，并把模型输出当作不可信代码。禁止sorry只是最低要求；还需审计新增公理、外部生成文件和宏展开结果。

证明依赖图比成功率更重要

若只统计“通过了多少目标”，团队可能得到一个无法维护的巨大脚本。更有价值的指标包括：每个引理依赖多少前置结论、最长依赖链、重复引理比例、自动化耗时、重建稳定性，以及定义变更后受影响的范围。把这些信息画成有向无环图，可以找出过度耦合的核心节点。

指标	风险信号	处理方式
单引理依赖过多	难以审计	拆分接口引理
自动化耗时波动大	搜索不稳定	固定策略或补中间结论
大量隐式类型推断	语义难读	在边界处显式标注
版本升级全局失败	耦合过深	锁版本并分层升级

对于重大数学结果，还应把关键定义和核心引理由独立团队重新形式化。两份实现若使用不同抽象仍得到一致结论，会比复制同一代码库更有说服力。

如何阅读“AI 解决难题”的新闻

第一，找到原始论文与形式化仓库，而不是只读新闻摘要。第二，确认形式命题与公认问题陈述之间的映射。第三，查看是否存在未证明占位、额外公理或无法复现的依赖。第四，区分作者验证、机器验证与外部同行评审。第五，等待专业共同体检查关键构造与边界情形。

正式宣布与最终接受之间可能经历较长时间。形式化能缩小逻辑错误空间，却不自动解决问题选择、语义对齐和学术评价。对企业研发同样如此：机器可验证的代码或证明可以成为质量闸门，但责任仍需明确的人类负责人承担。

搭建一个小型实验

选择一个已有纸面证明的基础定理，先由人手工建立形式定义与五到十个引理，再让模型只补全局部证明。每次候选输出进入干净容器编译，记录提示、代码差异、耗时、使用的公理和失败原因。最后由另一位成员在不看模型对话的情况下复核命题对齐。

实验的成功标准不是“模型写得比人快”，而是产物可重建、依赖清晰、没有未授权公理，且复核者能解释关键步骤。达到这些条件后，再扩大目标规模并引入检索、引理推荐或多轮修复。

结语与检查清单

AI 与形式化证明的强组合，是让模型探索候选论证，让小型内核承担确定性检查，再让专家负责命题对齐与学术判断。实践时确认：原命题逐项映射；工具链版本锁定；模型代码在隔离环境执行；禁止占位证明和新增公理；依赖图可审计；构建可复现；重大结论有独立复核。守住这七道门，形式化才是可信度放大器，而不是给未经审查的结论盖章。