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

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

• 作者：马丁·克勒普曼（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 生成的代码，就像我们从不查看编译器生成的机器码一样。

总结一下：

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

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

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 生成代码需形式验证以信任”高度一致。他乐观预测这将很快成为数学（及相关领域）主流。

证明助手（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 开始大幅降低证明成本。

主要应用领域

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

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

趋势

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

https://xjtu.app/t/topic/14671

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

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

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 代码，不仅修正了原论文中的各种不一致之处和漏洞，甚至证明了一些原本被省略的命题。

相关成果可见：
https://nasqret.github.io/ZsigmondyChebyshev/blueprint/index.html

我将陆续发布一系列此类实验，以证明在某些数学领域——包括初等数论、组合数学和分析（即 Mathlib 所涵盖的各类内容）——我们距离大规模转变数学证明有效性的文档方式已经不远了。我认为，这一年将会非常忙碌！

如果我是今天的一名学生，与最前沿的大语言模型互动几乎会让我觉得是在“作弊”。今天早上，我随手拍了一张黑板的照片，让 ChatGPT-5.2-Pro 解释其中的背景、解法，以及关于切瓦雷（Chevalley）关于可构造集（constructible sets）著名定理的一些补充评论。我收到的竟是一份极为深入的报告，它综合了来自全网的高质量代数几何材料，内容之精炼与深刻令人惊叹。

这引发了一个严肃的问题：当今学生真正面对的努力与挑战究竟是什么？成本固然是一个因素，但一旦能够使用这些模型，我们该如何在这个信息丰裕的时代学习？在这个时代，解释、参考文献和交互式探索几乎都能即时获取。

也许，真正的困难已不再是如何获得信息，甚至也不再是如何理解某个孤立的论证，而在于培养判断力：懂得提出什么样的问题，知道哪些解释值得信任，能够分辨深刻洞见与表面合理的区别，并将思想真正内化，而非仅仅消费内容。在一个答案唾手可得的环境中，真正的挑战或许在于如何形成品味、数学直觉，以及在知识突然泛滥的洪流中学会航行——而非沉没其中。

@HarmonicMath Building Mathematical Superintelligence

Harmonic 由 Robinhood 创始人兼 CEO Vlad Tenev 与 Tudor Achim 共同创立，致力于开发一种新型的人工智能系统——Mathematical Superintelligence（MSI，数学超智能），其目标是让 AI 具备接近甚至超越人类顶尖数学家的形式化推理与证明能力。

该实验室的代表性成果是名为 Aristotle 的 AI 系统。Aristotle 在 2025 年国际数学奥林匹克竞赛（IMO）中取得了历史性金牌水平的表现，并在标准数学推理评测（如 MiniF2F）上达到了 90% 的准确率。更引人注目的是，Aristotle 曾在6 小时内解决了一个困扰数学界 30 年的公开问题，展示了其强大的问题求解能力。

Harmonic 强调，真正的智能不应只关注答案，而应关注推理过程的正确性：“当我们想知道一个答案是否正确时，我们检查的是推理——那些逻辑步骤”。其长远愿景是让数学超智能不仅成为研究工具，还能被广泛、公平地使用：“数学超智能即将到来，它应当被均匀分布”。

截至 2025 年底，Harmonic 已获得1 亿美元融资并晋升为“独角兽”企业，显示出业界对其技术路线的高度认可。

Harmonic 的 x 账号被人工智能和数学领域的知名学者关注。

1. Chieh-Hsin (Jesse) Lai (@JC JesseLai)

   • 身份：目前是索尼 AI（Sony AI）的研究员，同时也是纽约城市大学（NYCU）应用数学系的访问助理教授。
   • 背景：拥有明尼苏达大学（U. of Minnesota）的数学博士学位。
   • 领域：他的研究横跨数学与人工智能，是扩散模型领域和流模型领域的领军人物，尤其关注扩散模型在音乐合成中的应用。他个人网站 chiehhshinjesselai.github.io 可能展示其更详细的研究成果。

2. Christian Szegedy (@ChrSzegedy)

   • 身份：人工智能领域的研究科学家。
   • 领域：他是深度学习领域的先驱之一，以其在计算机视觉和神经网络架构方面的工作而闻名。他参与了 Google Brain 团队，并对 Inception 架构等有重要贡献。
   • 观点：他明确表示“Opinions are mine.”（观点仅代表个人），表明他在社交媒体上分享的是个人见解。

3. Emily Riehl (@emilyriehl)

   • 身份：范畴论专家、在职数学家。
   • 领域：她是现代范畴论领域的领军人物，尤其在高阶范畴论和同伦理论方面有深入研究。她致力于将抽象的范畴论概念应用于更广泛的数学领域，并以清晰的教学风格著称，著有《Category Theory in Context》等教材。

4. François Chollet (@fchollet)

   • 身份：Keras 框架的创建者，ARC-AGI 和@ndea 的联合创始人，《Python 深度学习》一书的作者。
   • 领域：他是人工智能界最具影响力的人物之一。他开发的 Keras 库极大地简化了深度学习模型的构建过程，推动了该领域的普及。他目前专注于通用人工智能（AGI）的研究，特别是通过 ARC-AGI 竞赛来探索和评估机器的抽象推理能力。

入门形式化证明

1. 前提知识
   确保掌握离散数学基础：命题逻辑、谓词逻辑、归纳证明、集合论、函数。

2. 选择工具并入门证明助手
   推荐从Coq或Lean起步（两者是最流行、社区活跃的）。

   • 首选 Coq：工业应用多（如验证编译器 CompCert、操作系统内核），教程最成熟，适合 CS 学生。
   • 备选 Lean：更现代、数学友好（mathlib 库巨大，正在改变数学证明方式），语法简洁，适合对数学感兴趣的学生。
   • 为什么不先学 Isabelle？它自动化强，但入门曲线陡，不如 Coq/Lean 直观。

   学习路径：跟着官方互动教程一步步做练习。

3. 进阶

   • 验证简单程序（如排序算法、链表操作）的正确性。
   • 了解 Hoare 逻辑（程序正确性基础）。
   • 接触时序逻辑（并发系统验证）。
   • 后期可扩展到模型检查（Model Checking，如 SPIN 工具）或硬件验证（SVA 属性）。
   • 加入社区：Coq 的 Zulip、Lean's Zulip（非常活跃）。

材料

Coq 路线

• Software Foundations（简称 SF，最经典免费教材，由 UPenn 教授编写）：
  https://softwarefoundations.cis.upenn.edu/
  全套 5 卷，从逻辑基础到程序验证，用 Coq 互动练习。中文翻译版也有（搜索“软件基础”）。从 Volume 1 (Logical Foundations) 开始，非常适合新人。

南京大学 蒋炎岩 推荐 书目

• Coq 官方教程：Coq 官网文档 + 安装 Coq Platform（包含 VsCode 插件 Proof General 或 VSCoq）。

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

• Theorem Proving in Lean（官方互动教程）：
  https://leanprover.github.io/theorem_proving_in_lean4/
  简洁现代，从基础到高级。
• Mathematics in Lean：数学导向。
  https://leanprover-community.github.io/mathematics_in_lean/
• Natural Number Game（趣味互动游戏入门）：
  https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
  超级适合零基础，玩着玩就学会证明。

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

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

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 社区的广泛讨论。

https://arxiv.org/abs/2512.14575

Zulip 论坛

https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/AI-discovered.20proof.20on.20psi-integrals.20.28with.20Lean.20formalizat.2E.29/near/563828163

1. 背景与数学结果

• 问题来源：Schmitt 参与了一个叫IMProofBench的项目。这是一个专为测试 AI 在研究级数学证明能力的基准测试项目（private benchmark，避免数据污染）。项目收集了多名数学家提交的 PhD 水平开放问题。

• 具体问题：在稳定曲线模空间 $\overline{\mathcal{M}}_{g,n}$ 上，纯ψ类交数（descendant integrals）：

其中 $\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 代码：https://github.com/schmittj/balanced-vectors-blueprint

• 社区成员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 已在辅助研究级数学。

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

https://terrytao.wordpress.com/2025/12/08/the-story-of-erdos-problem-126/

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

Erdős 问题#1026 源于保罗·埃尔德什（Paul Erdős）对单调子序列的探究。该问题最初表述较为模糊：给定一个 distinct 实数序列 $a_1 < a_2 < \dots < 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 表示，该问题现已标记为“已解决”。这一协作模式或将成为未来攻克顽固开放问题的标准路径，预示着人工智能与形式化证明时代在数学领域的全面到来。

其他资料

• https://itp-conference.github.io/
• https://sigplan.org/Conferences/CPP/
• https://mathlib-initiative.org/
• https://pitmonticone.github.io/ItaLean2025/
• https://adam.math.hhu.de/#/
• https://adam.math.hhu.de/#/g/emilyriehl/ReintroductionToProofs
• Leibniz International Proceedings in Informatics
• https://harmonic.fun/

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

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

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

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

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

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

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

https://arxiv.org/abs/2601.22401