面向关注 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_code0andresult.unsolved_goals0andnotresult.forbidden_tokensandresult.axiomsresult.project_allowlist)代码是独立的工作流示意。真实系统还要锁定 Lean 与 mathlib 版本、限制网络、记录编译日志并把模型输出当作不可信代码。禁止sorry只是最低要求还需审计新增公理、外部生成文件和宏展开结果。证明依赖图比成功率更重要若只统计“通过了多少目标”团队可能得到一个无法维护的巨大脚本。更有价值的指标包括每个引理依赖多少前置结论、最长依赖链、重复引理比例、自动化耗时、重建稳定性以及定义变更后受影响的范围。把这些信息画成有向无环图可以找出过度耦合的核心节点。指标风险信号处理方式单引理依赖过多难以审计拆分接口引理自动化耗时波动大搜索不稳定固定策略或补中间结论大量隐式类型推断语义难读在边界处显式标注版本升级全局失败耦合过深锁版本并分层升级对于重大数学结果还应把关键定义和核心引理由独立团队重新形式化。两份实现若使用不同抽象仍得到一致结论会比复制同一代码库更有说服力。如何阅读“AI 解决难题”的新闻第一找到原始论文与形式化仓库而不是只读新闻摘要。第二确认形式命题与公认问题陈述之间的映射。第三查看是否存在未证明占位、额外公理或无法复现的依赖。第四区分作者验证、机器验证与外部同行评审。第五等待专业共同体检查关键构造与边界情形。正式宣布与最终接受之间可能经历较长时间。形式化能缩小逻辑错误空间却不自动解决问题选择、语义对齐和学术评价。对企业研发同样如此机器可验证的代码或证明可以成为质量闸门但责任仍需明确的人类负责人承担。搭建一个小型实验选择一个已有纸面证明的基础定理先由人手工建立形式定义与五到十个引理再让模型只补全局部证明。每次候选输出进入干净容器编译记录提示、代码差异、耗时、使用的公理和失败原因。最后由另一位成员在不看模型对话的情况下复核命题对齐。实验的成功标准不是“模型写得比人快”而是产物可重建、依赖清晰、没有未授权公理且复核者能解释关键步骤。达到这些条件后再扩大目标规模并引入检索、引理推荐或多轮修复。结语与检查清单AI 与形式化证明的强组合是让模型探索候选论证让小型内核承担确定性检查再让专家负责命题对齐与学术判断。实践时确认原命题逐项映射工具链版本锁定模型代码在隔离环境执行禁止占位证明和新增公理依赖图可审计构建可复现重大结论有独立复核。守住这七道门形式化才是可信度放大器而不是给未经审查的结论盖章。参考资料On the Navier–Stokes Millennium Prize Problem — OpenAI2026-09-08Theorem Proving in Lean 4 — Lean 官方教材The Lean Language Reference — 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_code0andresult.unsolved_goals0andnotresult.forbidden_tokensandresult.axiomsresult.project_allowlist)代码是独立的工作流示意。真实系统还要锁定 Lean 与 mathlib 版本、限制网络、记录编译日志并把模型输出当作不可信代码。禁止sorry只是最低要求还需审计新增公理、外部生成文件和宏展开结果。证明依赖图比成功率更重要若只统计“通过了多少目标”团队可能得到一个无法维护的巨大脚本。更有价值的指标包括每个引理依赖多少前置结论、最长依赖链、重复引理比例、自动化耗时、重建稳定性以及定义变更后受影响的范围。把这些信息画成有向无环图可以找出过度耦合的核心节点。指标风险信号处理方式单引理依赖过多难以审计拆分接口引理自动化耗时波动大搜索不稳定固定策略或补中间结论大量隐式类型推断语义难读在边界处显式标注版本升级全局失败耦合过深锁版本并分层升级对于重大数学结果还应把关键定义和核心引理由独立团队重新形式化。两份实现若使用不同抽象仍得到一致结论会比复制同一代码库更有说服力。如何阅读“AI 解决难题”的新闻第一找到原始论文与形式化仓库而不是只读新闻摘要。第二确认形式命题与公认问题陈述之间的映射。第三查看是否存在未证明占位、额外公理或无法复现的依赖。第四区分作者验证、机器验证与外部同行评审。第五等待专业共同体检查关键构造与边界情形。正式宣布与最终接受之间可能经历较长时间。形式化能缩小逻辑错误空间却不自动解决问题选择、语义对齐和学术评价。对企业研发同样如此机器可验证的代码或证明可以成为质量闸门但责任仍需明确的人类负责人承担。搭建一个小型实验选择一个已有纸面证明的基础定理先由人手工建立形式定义与五到十个引理再让模型只补全局部证明。每次候选输出进入干净容器编译记录提示、代码差异、耗时、使用的公理和失败原因。最后由另一位成员在不看模型对话的情况下复核命题对齐。实验的成功标准不是“模型写得比人快”而是产物可重建、依赖清晰、没有未授权公理且复核者能解释关键步骤。达到这些条件后再扩大目标规模并引入检索、引理推荐或多轮修复。结语与检查清单AI 与形式化证明的强组合是让模型探索候选论证让小型内核承担确定性检查再让专家负责命题对齐与学术判断。实践时确认原命题逐项映射工具链版本锁定模型代码在隔离环境执行禁止占位证明和新增公理依赖图可审计构建可复现重大结论有独立复核。守住这七道门形式化才是可信度放大器而不是给未经审查的结论盖章。参考资料On the Navier–Stokes Millennium Prize Problem — OpenAI2026-09-08Theorem Proving in Lean 4 — Lean 官方教材The Lean Language Reference — Lean 官方参考文档
