Lean 与 AI 合流：形式化证明库正在成为新一代「认知基建」
10 月 6 日 OpenAI 在 GitHub 的 openai/math 仓库公开了内部前沿模型产出的数学手稿与配套证明工件。波兰语媒体报道提到，其中一项关于离散几何关键猜想的结果，由一组外部数学家核验，并另写了伴随论文解释论证、补充背景与意义。技术圈普遍把这次发布读作一个信号：Lean 这类形式化证明系统，正从小众学术工具变成 AI 时代的认知基建。 为什么是 Lean 站到了台前 Lean 的核心能力，是把数学命题写成类型、把证明写成程序，再由内核逐步检查。过去它普及慢，是因为人学起来累、写起来慢。但这个痛点对 AI 恰好相反——模型写代码比写自然语言更顺手，形式化语言的严格语法反而成了它的主场。 于是出现了一个精妙的互补：人负责提出猜想、判断价值，AI 负责把海量路径形式化，Lean 内核负责逐行验证。三者咬合，形成一条「生成—形式化—验证」的流水线。 生态正在被重新点燃 从技术前沿看，变化有三： 证明工件公开化：手稿、证明脚本、复现环境一起进 GitHub，社区可以像审代码一样审数学。 外部核验制度化： advisory group 公开呼吁实验室停止在私有模型上测高等数学、改为公开结果，意味着同行审查在向 AI 成果延伸。 工具链成熟：Lean 与模型生成、外部评审、错误撤回的闭环跑通，证明这套基建可以承载真实产出。 保留 要泼的冷水是：公开仓库不代表全部复现成本已透明，「数百项」的清单仍待社区逐条消化；OpenAI 当天撤回 3 份、修订 14 份，说明形式化流水线也会引入它自己的错误。但方向是清楚的——当证明可以像代码一样被托管、评审、版本管理，数学就获得了它等待多年的软件工程化底座。 还有一点值得记录：advisory group 公开呼吁实验室停止在私有模型上测试高等数学、改为公开结果。这种「开放优于私有」的共识，对形式化数学生态是长期利好——只有工件公开，社区才能建起可复用的证明库，让后来者站在前一份形式化结果上继续堆叠，而不是每次都从零开始。 去论坛讨论 这篇文章里的观点，欢迎到硅基AGI论坛讨论。按标题搜索：Lean 与形式化数学