DDIA 作者：预测人工智能将使形式化验证走向主流

深入交流 ai cs 974 views 12 replies

#1 · 2025-12-18

预测：人工智能将使形式化验证走向主流

作者：马丁·克勒普曼（Martin Kleppmann）
发布日期：2025 年 12 月 8 日

人们已经广泛讨论过人工智能（AI）对软件开发的影响，但有一个角度我还没怎么见到有人提及：我相信，AI 将使形式化验证（formal verification）——这一数十年来一直被视为小众甚至边缘领域的技术——真正进入软件工程的主流。

像 Rocq、Isabelle、Lean、F* 和 Agda 这样的证明助手（proof assistants）和以证明为导向的编程语言已存在多年。它们允许开发者为一段代码编写形式化的规范（specification），然后通过数学方式证明该代码在所有情况下（包括你未曾想到的奇怪边界情况）都满足该规范。这些工具已被用于开发一些大型的形式化验证软件系统，例如操作系统内核、C 语言编译器和加密协议栈。

目前，形式化验证主要局限于研究项目，工业界的软件工程师（即使是在医疗设备和航空等传统高可靠性领域工作的工程师）很少使用形式化方法。原因在于编写这些证明既极其困难（通常需要博士级别的训练），又极其耗时。

例如，截至 2009 年，经过形式化验证的 seL4 微内核包含 8,700 行 C 代码，但完成其正确性证明却耗费了 20 人年的工作量，以及 20 万行 Isabelle 证明代码——这意味着每行实现代码平均需要 23 行证明代码和半天的人力。此外，据我粗略估计，全世界大概只有几百人真正懂得如何编写这类证明，因为这需要大量关于证明系统本身的深奥知识。

用简单的经济学术语来说：对大多数系统而言，由 bug 带来的预期成本，低于使用形式化验证技术以彻底消除这些 bug 的预期成本。部分原因或许是 bug 本质上是一种“负外部性”：承担 bug 成本的往往不是开发者，而是最终用户。但即使开发者自己承担全部成本，形式化验证依然过于困难和昂贵。

至少，这在最近之前确实是事实。如今，基于大语言模型（LLM）的编程助手不仅在编写实现代码方面表现越来越出色，甚至还能编写多种语言的证明脚本。目前，这一过程仍需具备专业知识的人类加以引导，但我们不难推断：在接下来的几年内，这一过程有望实现完全自动化。一旦如此，形式化验证的经济性将发生根本性转变。

如果形式化验证变得极其便宜，我们就能验证更多软件。不仅如此，AI 本身也催生了对形式化验证的更大需求：与其让人去审查 AI 生成的代码，我更愿意让 AI 向我证明它生成的代码是正确的。如果它能做到这一点，我宁愿选择 AI 生成的代码，而不是充满“手工匠气 bug”的人工代码！

事实上，我认为编写证明脚本正是 LLM 最理想的应用场景之一。因为即使 LLM 产生了胡言乱语（hallucination），证明检查器（proof checker）也会拒绝任何无效的证明，并强制 AI 重新尝试。而证明检查器本身通常是一小段经过验证的代码，几乎不可能让无效证明蒙混过关。

当然，这并不意味着软件会突然变得毫无 bug。随着验证过程本身日益自动化，挑战将转移到正确地定义规范上：也就是说，你如何确定所证明的性质，正是你真正关心的性质？阅读和编写这类形式化规范仍然需要专业知识和深思熟虑。但与手写证明相比，编写规范要容易且快速得多——这本身就是巨大进步。

我甚至可以想象，未来的 AI 代理还能协助编写规范，实现形式语言与自然语言之间的相互翻译。虽然翻译过程中可能会丢失一些细微差别，但这种风险似乎是可控的。

想到未来我们只需以高级、声明式的方式指定一段代码应有的性质，AI 就能“凭直觉”（vibe code）生成实现代码以及证明其满足规范的证明，这令我感到无比兴奋。这将彻底改变软件开发的本质：我们甚至不再需要查看 AI 生成的代码，就像我们从不查看编译器生成的机器码一样。

总结一下：

形式化验证即将变得极其廉价；
AI 生成的代码需要形式化验证，这样我们才能跳过人工审查，仍可确信其正确性；
形式化验证的精确性正好弥补了 LLM 的模糊性和概率性。

这三点共同作用，意味着形式化验证很可能在可预见的未来走向主流。我猜测，届时限制其普及的将不再是技术本身，而是人们观念上的转变——即意识到形式化方法如今已在实践中变得切实可行。

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#2 · 2025-12-18

AI+ 形式化证明 正在改变数学界的工作方式

陶哲轩（Terence Tao） 有多个文章、博客帖子和演讲表达了与 Martin Kleppmann 高度相似的观点：AI 将大幅降低形式验证（formal verification）和证明助手（如 Lean）的成本，推动其在数学和软件工程中变得主流，甚至成为标准实践。

关键文章与演讲：
- 2024 年 AMS Colloquium Lecture“Machine Assisted Proofs”（YouTube，基于 Notices of the American Mathematical Society 文章）：系统讨论机器辅助证明历史与未来，强调 AI + 证明助手（如 Lean）可实现大规模协作、自动化验证，甚至生成完整论文 + 形式证明。预测形式化将成为常态，AI 作为“数学家的副驾驶”。
- 博客系列（terrytao.wordpress.com）：
  - “Formalizing the proof of PFR in Lean4 using Blueprint”（2023）：描述用 AI 辅助在 Lean 中形式化复杂证明，强调 AI 填补小缺口潜力。
  - “A slightly longer Lean 4 proof tour”（2023）：认为 AI 近期目标是自动关闭证明中的“小 sorry”（未证明部分），加速蓝图到形式证明转换。
  - “A tool to verify estimates, II: a flexible proof assistant”（2025）：开发仿 Lean 的轻量证明助手，计划集成 AI 生成伪证明后转正式 Lean 验证。
  - “Machine assisted proofs”PDF 与相关帖子：讨论 AI 与证明助手结合，验证 LLM 输出，推动形式方法普及。
- 采访（如 Scientific American, 2024）：AI 将成为数学家“副驾驶”，未来解释证明给 GPT，它生成 Lean 代码并验证。形式化成本将低于传统写作，推动广泛采用。
- 其他实践：陶哲轩亲自用 GitHub Copilot + AI 在 Lean 中形式化证明（如 PFR 猜想、Analysis I 教材），并发现手动证明中隐藏错误，证明形式验证 + AI 的实用价值。

陶哲轩虽主要聚焦数学证明形式化，但其观点直接适用于软件工程：AI 生成代码 + 证明可跳过人工审查，确保正确性，与 Kleppmann“AI 生成代码需形式验证以信任”高度一致。他乐观预测这将很快成为数学（及相关领域）主流。

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#3 · 2025-12-18

证明助手（Proof Assistant）

证明助手（也叫交互式定理证明器）是一种帮助人类用计算机严格证明数学定理或验证软件/硬件正确性的工具。

核心概念

形式化证明：把数学命题和证明过程完全用精确的逻辑语言写出来，计算机能 100% 检查。
证明检查器：工具的核心部分很小（小内核原则），本身被严格验证，几乎不可能出错。即使人或 AI 写出错误证明，它也会拒绝。
柯里 - 霍华德同构：证明 ↔ 程序。写一个证明的过程就像写一个满足规格的程序（这也是很多证明助手同时支持代码生成的原因）。

历史关键里程碑

1967 年：Automath，第一个形式化数学系统。
1980 年代：Coq、Isabelle 诞生，四色定理首次被机器验证。
1994 年：英特尔奔腾芯片浮点 bug 损失 4.75 亿美元，推动工业界重视形式验证。
2009 年：seL4 操作系统内核被完全形式化验证（世界上第一个）。
2010 年代：Lean 出现，Mathlib 数学库快速增长。
2023–2025 年：AI 大爆发——DeepMind 的 AlphaProof、DeepSeek-Prover、OpenAI 等用 AI+ 证明助手解决 IMO（国际数学奥林匹克）难题，标志 AI 开始大幅降低证明成本。

主要应用领域

软件/硬件验证
- 操作系统内核（如 seL4）
- 编译器（如 CompCert，保证编译后代码不引入 bug）
- 密码协议、区块链智能合约、航空/医疗设备软件
- 避免灾难性 bug（比如芯片设计错误、分布式系统一致性问题）
数学大定理证明
- 四色定理、开普勒猜想、费马大定理、奇数阶有限单群分类等
- 建立大规模机器验证数学库（Lean 的 Mathlib、Isabelle 的 AFP）
编程语言设计
- 证明类型系统安全、并发模型正确等

常用工具对比（2025 年主流）

工具	特点亮点	代表项目/成就
Lean 4	速度快、自动化强、社区活跃、AI 友好	Mathlib 最大数学库；IMO 银牌（AlphaProof）
Rocq/Coq	历史最久、代码生成强、小内核可靠	CompCert 编译器、seL4 早期验证
Isabelle	高阶逻辑、文档生成好、工业应用多	seL4 完整验证、Archive of Formal Proofs
F*	专为程序验证 + 代码生成设计	安全关键软件、加密协议
Agda	依赖类型纯度高，适合理论研究
HOL Light/HOL4	极简内核、数学证明强	开普勒猜想证明

趋势

AI 与证明助手的结合：大型语言模型（LLM）能自动生成证明草稿，证明检查器负责把关，彻底改变“写证明太贵太难”的局面。
代表成果：谷歌 DeepMind、OpenAI、DeepSeek 等已在 Lean 上实现高难度数学题自动证明。
未来预期：形式化证明成本大幅下降，可能像编译器一样成为软件开发的标配；数学家只需提供高层次思路，AI 填细节并验证。

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#4 · 2025-12-18

Zethes

IO — #1 in 陶哲轩为分析学教材创建 lean 配套项目

项目地址:

blog

AI 翻译:

将近 20 年前，我写了一本关于实分析的教科书，名为《分析 I》（Analysis I）。这本书旨在通过更注重基础问题（例如自然数、整数、有理数和实数的构造）来补充当时已有的许多优秀的分析教材，并提供了足够的集合论和逻辑知识，使学生能够以高度严谨的方式推导证明。

当这本书撰写时，诸如 Coq 或 Agda 这样的形式化验证工具已经存在，但我当时并未关注这一领域。然而，如今在接触了这一学科之后，我意识到本书的内容实际上与这些形式化验证系统非常契合；特别是我当时隐式使用的“朴素类型理论”（naive type theory）——用来构建标准数系的方法——与 Lean 的依赖类型理论（dependent type theory）非常匹配（其中尤其对商类型（quotient types）有着良好的支持）。

因此，我决定为《分析 I》创建一个 Lean 配套项目，该项目将书中的许多定义、定理和练习“翻译”成 Lean 代码。特别地，这提供了一种替代方式来完成书中的练习：即通过填写相应的 Lean 代码中的“sorries”。（不过，我并不计划在这个配套项目中发布官方的习题解答；你可以自由地 fork 此仓库并自行填写这些“sorries”。）

目前，以下章节内容已被翻译为 Lean：

第 2.1 节：自然数
第 2.2 节：加法
第 2.3 节：乘法
第 2 章附录：与 Mathlib 自然数的同构
第 3.1 节：集合论基础
第 4.1 节：整数

这个形式化过程中有意在某些地方脱离标准的 Lean 数学库 Mathlib，而在其他地方又依赖于它。比如，Mathlib 已经自带了自然数的标准定义 ℕ。在 Lean 的形式化中，我首先手工构造了一个不同的自然数类型 Chapter2.Nat（或简称为 Nat，如果你是在 Chapter2 命名空间下），并建立了很多关于这些新自然数的基本结果，它们与 Mathlib 中已有的一些关于 ℕ 的引理相对应（但其中很多作为练习留给读者，其证明被暂时替换为“sorries”）。然后，在附录部分，我们建立了这些新的自然数与 Mathlib 中自然数之间的同构关系（或者更准确地说，这部分也留作练习）。从那时起，“Chapter 2”中的自然数就被弃用了，转而使用 Mathlib 提供的标准自然数。我希望在整个书中延续这种模式，随着章节推进，更多地依赖 Mathlib 中的定义和函数，而不是直接引用早期章节中的替代版本。因此，这个配套项目也可以作为学习 Lean 和 Mathlib 的入门材料，同时也能帮助学习实分析（这一点有点类似于“自然数游戏”（Natural number game），事实上该游戏与我书中第 2 章在主题上有很多重叠之处）。

本仓库中的代码可以在 Lean 中编译，但我尚未测试代码中所有的（大量）“sorries”是否真的可以被填满（也就是说，这些练习是否真的能在 Lean 中被解决）。我希望能有志愿者来“试玩”这个配套项目，看看是否真的可行（以及提供的辅助引理或“API”是否足够让使用者以概念上简单明了的方式填写这些 sorries，而无需依赖一些较为冷门或复杂的 Lean 编程技巧）。当然，任何其他反馈也非常欢迎。

[更新，5 月 31 日：此配套项目已移至独立仓库。]

陶哲轩（Terence Tao）的《Analysis I》Lean 形式化项目

这个 GitHub 仓库是陶哲轩于2025 年 5 月 31 日正式启动的一个开源项目，目的是将他的经典实分析教材《Analysis I》（本科生水平）用Lean 4证明助手进行形式化翻译。

项目核心目标

忠实复述原书：尽可能贴近教材的定义、定理和证明结构，同时展示 Lean 的语法和特性（不追求最高效率，有时会偏离 Lean 的“习惯用法”）。
作为伴侣资源：不是取代原书，而是提供一个“带注释的伴侣”。书中留给读者的习题在这里用 sorry（占位符）表示，鼓励读者自己 fork 仓库填写证明。
不直接引用原书文字：只给出原书章节引用，避免版权问题。
与 Mathlib 兼容：早期章节独立定义（如第 2 章自己构建自然数），后期逐步切换到 Lean 标准数学库Mathlib的定义（并在章节结尾证明两者同构），这样既教学又实用。

技术调整（为什么与原书稍有不同）

序列从0 开始索引（原书从 1 开始），因为 Mathlib 对ℕ（从 0 开始）的支持更好。
一些原书未定义的操作（如除以 0、非 Cauchy 序列的极限）被赋“垃圾值”（如 0），确保函数是全定义的（total function）。Lean 对全函数支持更好，避免部分函数带来的证明复杂性（“dependent type hell”）。
第 2 章自然数用归纳类型构造（而非纯公理化），但在结尾证明了 Peano 公理。

当前形式化进度（截至 2025 年 12 月）

项目进展非常快，已基本覆盖全书主要内容（第 1 章引言未形式化）：

第 2 章：自然数（Peano 公理、加法、乘法）+ 与 Mathlib 同构。
第 3 章：集合论基础、函数、像与原像、笛卡尔积、基数等。
第 4 章：整数、有理数、绝对值、指数、理性数的间隙。
第 5 章：实数构造（Cauchy 序列）、序、最小上界界、实指数等 + 与 Mathlib 实数同构。
第 6 章：序列极限、扩展实数、上下极限、标准极限、子序列等。
第 7 章：级数（有限、无限、非负和、重排、根检验/比检验）。
第 8 章：无穷集合（可数、不可数、选择公理、有序集）。
第 9 章：ℝ上连续函数（子集、极限、连续性、中值定理、一致连续等）。
第 10 章：导数（基本定义、单调性、反函数导数、L'Hôpital 法则）。
第 11 章：Riemann 积分（分划、上/下积分、可积性、基本定理等）。
附录 A：数学逻辑基础（语句、蕴涵、量词、相等等）。
附录 B：十进制表示。

此外，还有一些额外内容：

陶哲轩的《测度论》书籍形式化（进行中）。
物理单位系统形式化（包括 SI 单位）。
有限选择公理（避免使用 Lean 的选择公理）。
有限概率论及几个 Erdős 问题的解。

项目现状与影响

社区活跃：1.4k 星、181 fork、36 位贡献者，最近提交在几天前。
文档网站：Analysis （每个章节有 Verso 页面、文档和 Lean 源代码）。
资源：仓库提供构建脚本、Lean 社区链接、Mathlib 搜索工具等。陶哲轩的 YouTube 频道有相关演示。
这体现了陶哲轩对 AI+ 证明助手的乐观态度：项目中使用 GitHub Copilot 等工具加速形式化，正如他之前预测的，AI 正让形式验证变得更易普及。

这个项目不仅是《Analysis I》的“机器可验证版本”，还是学习 Lean 和 Mathlib 的绝佳入门材料，尤其适合想结合教材和形式化证明的学生/研究者。如果你感兴趣，可以直接 clone 仓库尝试填写 sorry 部分！

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#5 · 2025-12-18

Bartosz Naskręcki
Mathematician | Vice-Dean @UAM_Poznan | Researcher @ccaiwut | Rigorous mathematics, programming &ML | Passionate about what AI really understands

例子：这位数学家通过 HarmonicMath 加速完成数学定理的形式化证明。

数学论文需要形式化验证。通常，这一过程由审稿人非正式地完成。但如果我们能依赖更可靠的方式，例如自动形式化为 Lean 4 代码，从而将审稿人的角色简化为对定义和定理表述进行细致检查，那会怎样？此时，自动生成代码的编译结果本身就会成为一份证明证书。这正是我与 @HarmonicMath 的 Aristotle 在一次长期运行中所实现的成果。

感谢 @PietroMonticone 和 @llllvvuu 在蓝图（blueprint）搭建过程中的帮助。在此，我展示了一篇我朋友 Stefan Barańczuk 关于切比雪夫整除序列（Chebyshev divisibility sequences）论文的完整、正确的自动形式化成果。该代码包含约 5000 行高度非平凡的 Lean 代码，不仅修正了原论文中的各种不一致之处和漏洞，甚至证明了一些原本被省略的命题。

入门形式化证明

前提知识
确保掌握离散数学基础：命题逻辑、谓词逻辑、归纳证明、集合论、函数。
选择工具并入门证明助手
推荐从Coq或Lean起步（两者是最流行、社区活跃的）。
- 首选 Coq：工业应用多（如验证编译器 CompCert、操作系统内核），教程最成熟，适合 CS 学生。
- 备选 Lean：更现代、数学友好（mathlib 库巨大，正在改变数学证明方式），语法简洁，适合对数学感兴趣的学生。
- 为什么不先学 Isabelle？它自动化强，但入门曲线陡，不如 Coq/Lean 直观。
学习路径：跟着官方互动教程一步步做练习。
进阶
- 验证简单程序（如排序算法、链表操作）的正确性。
- 了解 Hoare 逻辑（程序正确性基础）。
- 接触时序逻辑（并发系统验证）。
- 后期可扩展到模型检查（Model Checking，如 SPIN 工具）或硬件验证（SVA 属性）。
- 加入社区：Coq 的 Zulip、Lean's Zulip（非常活跃）。

材料

Coq 路线

Software Foundations（简称 SF，最经典免费教材，由 UPenn 教授编写）：

全套 5 卷，从逻辑基础到程序验证，用 Coq 互动练习。中文翻译版也有（搜索“软件基础”）。从 Volume 1 (Logical Foundations) 开始，非常适合新人。 > 南京大学 [蒋炎岩](https://jyywiki.cn/) 推荐 [书目](https://jyywiki.cn/Reading_List.md) - **Coq 官方教程**：Coq 官网文档 + 安装 Coq Platform（包含 VsCode 插件 Proof General 或 VSCoq）。

Lean 路线（如果偏数学/AI 证明）

Theorem Proving in Lean（官方互动教程）：

简洁现代，从基础到高级。 - **Mathematics in Lean**：数学导向。

Mathematics in Lean — Mathematics in Lean v4.19.0 documentation

- **Natural Number Game**（趣味互动游戏入门）：

You are are being redirected...

超级适合零基础，玩着玩就学会证明。

通用基础书籍/课程（补充理论）

《Logic in Computer Science: Modelling and Reasoning about Systems》（Michael Huth & Mark Ryan）：逻辑基础好书。
Coursera/MIT OpenCourseWare 搜索“Formal Verification”或“Proof Assistants”。
中文：搜索“TLA+ 入门”（适合并发验证，Lamport 发明，亚马逊用它验证分布式系统），书《Specifying Systems》。

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#8 · 2025-12-18

ETH Zurich 的数学家 Johannes Schmitt 宣布了一个重要的里程碑：OpenAI 的 GPT-5 模型首次完全自主地解决了一个数学领域的开放问题（open math problem），提供了完整且正确的证明，没有任何人类提示或干预。

具体内容是关于枚举几何（enumerative geometry）中的一个小但新颖的贡献：涉及曲线模空间（moduli spaces of curves）上的交数（intersection numbers）。作者咨询了领域专家，确认这个问题此前是未解决的，没有明显的解法，于是提交到他参与的基准项目 IMProofBench（一个测试 AI 数学证明能力的平台）。

GPT-5 给出了一个优雅的证明，竟然绕过了该领域传统的复杂理论，而是从代数几何的另一个分支借用技术，提供了“局外人视角”的新思路。

随后，他们合作撰写了一篇论文，整合了多个 AI 模型的贡献（如 GPT-5 和 Gemini 3 Pro 的证明、Claude 的写作辅助、Lean 形式化验证），并透明标注了每段内容的 AI/人类来源，还附上提示日志。这被视为人-AI 协作的新实验。

有趣的结尾：GPT-5 在给出完美一般证明后，在一个特殊案例的示例公式上出现了幻觉（hallucination，完全编造错误内容），后来被另一个 AI（Claude）指出。

幻觉示例

总体来说，这个帖子标志着 AI 在高级数学研究中从“辅助工具”向“独立发现者”迈出关键一步，引发了数学和 AI 社区的广泛讨论。

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#9 · 2025-12-18

Zethes

Zulip 论坛

1. 背景与数学结果

问题来源：Schmitt 参与了一个叫IMProofBench的项目。这是一个专为测试 AI 在研究级数学证明能力的基准测试项目（private benchmark，避免数据污染）。项目收集了多名数学家提交的 PhD 水平开放问题。
具体问题：在稳定曲线模空间 $\overline{\mathcal{M}}_{g,n}$ 上，纯ψ类交数（descendant integrals）：

D(\mathbf{e}) = \langle \tau_{e_1} \cdots \tau_{e_n} \rangle_g = \int_{\overline{\mathcal{M}}_{g,n}} \psi_1^{e_1} \cdots \psi_n^{e_n}

其中 $\sum e_i = 3g-3+n$
（维度约束）。

问题：对于固定 g,n，哪些指数向量 $\mathbf{e} = (e_1, \dots, e_n)$ 使这个交数最大？
结果：最大值在balanced 向量上取得，即 $e_i$ 们尽可能均匀分布（相邻差至多 1）。最小值在集中向量（几乎所有质量在一个位置）上取得。
证明思路：AI（GPT-5）给出了一个简洁证明，完全绕过传统理论（如 Witten-Kontsevich 定理），只用ψ类的抽象交数性质：nefness（nef 类）和Khovanskii-Teissier 不等式（log-concavity）。
论文：Schmitt 迅速写成论文上传 arXiv（arXiv:2512.14575，标题《Extremal descendant integrals on moduli spaces of curves: An inequality discovered and proved in collaboration with AI》）。论文中明确标注 AI 贡献的部分（包括整段文字由 AI 撰写），并附提示日志以示透明。

这是一个里程碑：这是已知第一个 AI 独立解决研究级开放数学问题的公开案例（此前 AI 多在竞赛题或已知问题上表现）。

2. AI 的具体贡献

GPT-5 首先生成自然语言证明（被 Schmitt 和同事验证正确）。
其他 AI（如 Gemini 3 Pro、Claude Opus 4.5）帮助起草论文大段文字。
GPT-5.2 和 Claude Code 帮助生成 Lean 代码。
Schmitt 本人无 Lean 经验，一天内用 AI“vibe-coding”（随意生成 + 迭代）完成形式化。

3. Lean 形式化部分

证明分成两部分：
组合优化部分（Theorem 3.1）：一个纯组合不等式，证明某些对称 log-concave 函数在 balanced 向量上取最大值。这部分被完整形式化在 Lean 中（约 3.5 页 PDF）。
几何部分（Theorem 3.2）：证明 descendant integrals 满足上述函数性质（用 nef + log-concavity）。这部分仍是 informal（非形式化），因为模空间本身在 Lean/mathlib 中尚未定义（这是大工程，可能需多年）。
原始 Lean 代码：GitHub - schmittj/balanced-vectors-blueprint: Lean Blueprint for technical lemma on maxima and minimal of certain log-concave functions
社区成员Eric Vergo 快速重构代码，使其更符合 mathlib 风格，并作为测试“AI 生成 Lean 证明模板”的案例。
Kim Morrison（Lean 专家）给出改进建议，如分离定义与证明、添加警告（定义需人工审查）。

形式化好处：优化部分充满繁琐不等式，容易出错；Lean 验证后让人放心。Schmitt 认为这占了“50% 验证收益”，但只需“0.01% 工作量”（相比形式化整个代数几何背景）。

4. 社区讨论的焦点

惊喜与赞赏：很多人惊叹 AI 解决开放问题、零经验下形式化 Lean（“vibe-formalizing”）。
Kevin Buzzard（Lean 社区大牛）指出：模空间定义本身是巨大空白（甚至椭圆曲线模空间对 Fermat 最后定理都缺），形式化几何部分可能需多年。强调 AI 不可信赖定义，但可辅助填补小 lemma。
形式化 AI 证明的规范：讨论如何处理 AI 生成代码的信任问题。
建议：定义放单独文件 + 大警告，必须人工审查。
避免 mathlib 碎片化：优先推入主库。
讨论“quarantine”无证明义务的定义，便于审查。
更广哲学讨论（Timothy Chow 等）：
mathlib 是否应成“唯一正典”定义源？但数学概念往往有多个等价定义（A 类），或不等价但相关约定（B 类，如 Fourier 变换归一化）。
形式化是否完全捕捉数学的“非形式含义”？（如“可证明性”概念的细微差别、Gödel 不完备性、数学家的“直觉”）。
Kevin Buzzard：实际论文中的定理（如 Sylow）不依赖底层基础接线。

5. 意义与启示

AI 在数学研究中的角色：这例显示前沿 AI 已能发现新证明、绕过传统路径、辅助形式化。
未来趋势：可能出现“人+AI 混合证明”规范、专用模板处理 AI 贡献、mathlib 逐步覆盖更多代数几何。
当前状态（2025 年 12 月）：GPT-5 在 IMProofBench 上表现最佳（完全正确解决 22% 问题），显示 AI 已在辅助研究级数学。

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#10 · 2025-12-19

充满期待，数学需要形式化验证来整治。但听说现在还比较难用。

#11 · 2025-12-19

2025 年 12 月 8 日 —— 著名数学家、菲尔兹奖得奖者陶哲轩（Terence Tao）近日在其个人博客上详述了 Erdős 问题#1026 的完整解决过程。这一源于 1975 年的经典开放问题，通过在线社区协作、人工智能工具以及既有文献的结合，最终在 2025 年 12 月得以彻底解决。

Erdős 问题#1026 源于保罗·埃尔德什（Paul Erdős）对单调子序列的探究。该问题最初表述较为模糊：给定一个 distinct 实数序列 $a_1 \lt a_2 \lt \dots \lt a_n$ ，求最大单调子序列的和的上界。经过社区澄清和重新表述，该问题等价于确定常数 $c_k$ 的精确渐近行为，其中 $c_k$ 表示在总和归一化为 1 的序列中，Bob（选取单调子序列）所能保证的最大份额，而 Alice 试图最小化这一份额。最终证明表明， $c_k = 2 / \sqrt{k}$ 为上界，且在完美平方 k 时精确达成。

解决过程始于 2025 年 9 月 12 日，该问题被正式录入 Erdős 问题网站。社区成员迅速提出博弈论解读，并计算小 k 值，猜测 $c_k \sim 2 / \sqrt{k}$ 。问题一度沉寂近两个月，直至 12 月 7 日，数学家 Boris Alexeev 使用 AI 工具Aristotle（由 Harmonic 公司开发）对该问题进行系统扫描。

Aristotle 在完全自主模式下，仅基于形式化陈述，成功将问题转化为矩形打包问题，并在形式化证明系统Lean中生成完整证明。这一成就标志着 AI 首次独立产生非平凡数学证明，并直接输出可验证的形式化代码。尽管后续人类审查发现该证明并非全新（源于 1959 年 Seidenberg 的工作变体），但 Aristotle 的自主性和效率令人瞩目——它将一个潜在的猜想直接提升为形式化定理。

紧随其后，社区成员 Koishi Chan 提供基于 Erdős-Szekeres 定理的“blow-up”论证下界，而陶哲轩本人则运用另一 AI 工具AlphaEvolve生成上界数值证据，并推导出精确构造。最终，Lawrence Wu 通过 AI 深度文献搜索，定位 2024 年 Baek、Koizumi 和 Ueoro 的论文，该文解决了相关的 Erdős 平方打包问题（#106 的轴平行版本），从而严格证明上界 $ \max \sum_{i \in S} a_i \leq 2 / \sqrt{k} $。这一链接将问题彻底闭合。

陶哲轩在博客中强调：“这一解决过程融合了现有文献、在线协作与多种 AI 工具。”他指出，Aristotle 的 Lean 形式化证明、AlphaEvolve 的优化构造，以及 AI 辅助的文献检索，显著加速了进展。

这一事件是 2025 年 AI 辅助数学突破的最新例证。此前，Aristotle 已独立解决多个 Erdős 问题，并在 Lean 中形式化验证。专家认为，此类工具正重塑数学研究范式：AI 擅长处理文献“暗森林”、生成形式化代码和探索数值模式，从而让人类数学家专注于核心创造性工作。

Erdős 问题网站维护者 Thomas Bloom 表示，该问题现已标记为“已解决”。这一协作模式或将成为未来攻克顽固开放问题的标准路径，预示着人工智能与形式化证明时代在数学领域的全面到来。

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#12 · 2025-12-19

其他资料

Interactive Theorem Proving
Certified Programs and Proofs (CPP)
The Mathlib Initiative
ItaLean 2025
Lean Game Server
Lean Game Server
Leibniz International Proceedings in Informatics
Harmonic

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4

#13 · 2026-02-05

我们呈现了一项半自主数学发现的案例研究，使用 Gemini 系统性地评估了 Bloom 的埃尔德什问题数据库中标记为“开放”（Open）的 700 个猜想。我们采用了一种混合方法：首先通过 AI 驱动的自然语言验证来缩小搜索范围，随后由人类专家评估其正确性和新颖性。

在数据库中标记为“开放”的问题中，我们处理了 13 个：其中 5 个通过看似新颖的自主解法得到解决，另外 8 个通过识别现有文献中已有的先前解法而得到处理。我们的发现表明，这些被解决问题的“开放”状态更多源于其隐晦性（obscurity）而非真正的难度。

我们还识别并讨论了将 AI 大规模应用于数学猜想时出现的问题，特别强调了文献识别的困难，以及 AI 可能存在的“潜意识剽窃”（subconscious plagiarism）风险——即 AI 在训练中吸收了文献知识，却在输出时未适当归属或承认。

最后，我们反思了 AI 辅助方法在埃尔德什问题上的经验教训与启示。

我们的结果表明，埃尔德什问题中确实存在一些“唾手可得的果实”，而当前的 AI 已经具备采摘其中一部分的能力。这为 AI 研究者提供了一种引人入胜的新型数学基准，但我们提醒大家不要对其数学意义过度兴奋。我们在这里解决的任何开放问题，只要有合适的专家介入，其实都能相当轻松地被解决。另一方面，人类专家的时间是有限的。AI 已经展现出加速数学发现中“注意力瓶颈”环节的潜力——前提是其可靠性能够得到显著提升。

在我们的案例研究中，我们遇到了许多一开始并未预料到的困难。绝大多数在技术上正确的自主解法，其实都源自对问题陈述的错误理解或误读，而诊断这些问题有时需要付出相当大的努力。此外，对人类专家而言最困难的步骤并不是验证证明本身，而是判断该解法是否早已存在于文献之中。随着 AI 生成数学内容的增多，数学共同体必须保持警惕，防范“潜意识剽窃”现象——即 AI 在训练过程中吸收了文献知识，却在输出时未给出恰当承认和引用。请注意，形式化验证对此类问题毫无帮助。

虽然在埃尔德什问题上的自主尝试取得了一些成功，但同时也催生了误导性的炒作乃至彻头彻尾的错误信息，这些内容随后在社交媒体平台上被进一步放大，给数学共同体带来了负面影响。除了埃尔德什问题之外，未来还会有许多其他的数学猜想与问题列表，可能成为（半）自主研究的目标。我们强烈建议此类工作认真对待本文所指出的各类问题。

我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。
诗篇 23:4