{"topic":{"id":15280,"title":"DDIA 作者：预测人工智能将使形式化验证走向主流","slug":"topic","userId":7639,"categoryId":11,"createdAt":"2025-12-18 18:16:04.55562","bumpedAt":"2026-02-05 20:10:40.864645","views":924,"postsCount":13,"highestPostNumber":13,"likeCount":5,"closed":false,"pinned":false,"pinnedGlobally":false,"pinnedAt":null,"pinnedUntil":null,"isBanner":false,"excerpt":"预测：人工智能将使形式化验证走向主流作者：马丁·克勒普曼（Martin Kleppmann）发布日期：2025 年 12 月 8 日人们已经广泛讨论过人工智能（AI）对软件开发的影响，但有一个角度我还没怎么见到有人提及：我相信，AI 将使形式化验证（formal verification）——这一数十年来一直被视为小众甚至边缘领域的技术——真正进入软件工程的主流。像 Rocq、Isabelle、Lean、F* 和 Agda 这样…","deletedAt":null,"isAnonymous":false,"isPrivate":false,"isMembersOnly":false,"category":{"id":11,"name":"深入交流","slug":"distilled","color":"c01c28"},"author":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null},"realAuthor":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null},"tags":["ai","cs"]},"posts":[{"id":69056,"postNumber":1,"raw":"## 预测：人工智能将使形式化验证走向主流\n\n- 作者：马丁·克勒普曼（Martin Kleppmann） \n- 发布日期：2025 年 12 月 8 日\n\n人们已经广泛讨论过人工智能（AI）对软件开发的影响，但有一个角度我还没怎么见到有人提及：我相信，AI 将使形式化验证（formal verification）——这一数十年来一直被视为小众甚至边缘领域的技术——真正进入软件工程的主流。\n\n像 Rocq、Isabelle、Lean、F* 和 Agda 这样的证明助手（proof assistants）和以证明为导向的编程语言已存在多年。它们允许开发者为一段代码编写形式化的规范（specification），然后通过数学方式证明该代码在所有情况下（包括你未曾想到的奇怪边界情况）都满足该规范。这些工具已被用于开发一些大型的形式化验证软件系统，例如操作系统内核、C 语言编译器和加密协议栈。\n\n目前，形式化验证主要局限于研究项目，工业界的软件工程师（即使是在医疗设备和航空等传统高可靠性领域工作的工程师）很少使用形式化方法。原因在于编写这些证明既极其困难（通常需要博士级别的训练），又极其耗时。\n\n例如，截至 2009 年，经过形式化验证的 seL4 微内核包含 8,700 行 C 代码，但完成其正确性证明却耗费了 20 人年的工作量，以及 20 万行 Isabelle 证明代码——这意味着每行实现代码平均需要 23 行证明代码和半天的人力。此外，据我粗略估计，全世界大概只有几百人真正懂得如何编写这类证明，因为这需要大量关于证明系统本身的深奥知识。\n\n用简单的经济学术语来说：对大多数系统而言，由 bug 带来的预期成本，低于使用形式化验证技术以彻底消除这些 bug 的预期成本。部分原因或许是 bug 本质上是一种“负外部性”：承担 bug 成本的往往不是开发者，而是最终用户。但即使开发者自己承担全部成本，形式化验证依然过于困难和昂贵。\n\n至少，这在最近之前确实是事实。如今，基于大语言模型（LLM）的编程助手不仅在编写实现代码方面表现越来越出色，甚至还能编写多种语言的证明脚本。目前，这一过程仍需具备专业知识的人类加以引导，但我们不难推断：在接下来的几年内，这一过程有望实现完全自动化。一旦如此，形式化验证的经济性将发生根本性转变。\n\n如果形式化验证变得极其便宜，我们就能验证更多软件。不仅如此，AI 本身也催生了对形式化验证的更大需求：与其让人去审查 AI 生成的代码，我更愿意让 AI 向我证明它生成的代码是正确的。如果它能做到这一点，我宁愿选择 AI 生成的代码，而不是充满“手工匠气 bug”的人工代码！\n\n事实上，我认为编写证明脚本正是 LLM 最理想的应用场景之一。**因为即使 LLM 产生了胡言乱语（hallucination），证明检查器（proof checker）也会拒绝任何无效的证明，并强制 AI 重新尝试**。而证明检查器本身通常是一小段经过验证的代码，几乎不可能让无效证明蒙混过关。\n\n当然，这并不意味着软件会突然变得毫无 bug。随着验证过程本身日益自动化，挑战将转移到正确地定义规范上：也就是说，你如何确定所证明的性质，正是你真正关心的性质？阅读和编写这类形式化规范仍然需要专业知识和深思熟虑。但与手写证明相比，编写规范要容易且快速得多——这本身就是巨大进步。\n\n我甚至可以想象，未来的 AI 代理还能协助编写规范，实现形式语言与自然语言之间的相互翻译。虽然翻译过程中可能会丢失一些细微差别，但这种风险似乎是可控的。\n\n想到未来我们只需以高级、声明式的方式指定一段代码应有的性质，AI 就能“凭直觉”（vibe code）生成实现代码以及证明其满足规范的证明，这令我感到无比兴奋。这将彻底改变软件开发的本质：我们甚至不再需要查看 AI 生成的代码，就像我们从不查看编译器生成的机器码一样。\n\n总结一下： \n1. 形式化验证即将变得极其廉价； \n2. AI 生成的代码需要形式化验证，这样我们才能跳过人工审查，仍可确信其正确性； \n3. 形式化验证的精确性正好弥补了 LLM 的模糊性和概率性。 \n\n这三点共同作用，意味着形式化验证很可能在可预见的未来走向主流。我猜测，届时限制其普及的将不再是技术本身，而是人们观念上的转变——即意识到形式化方法如今已在实践中变得切实可行。","cooked":"

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

作者：马丁·克勒普曼（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 的模糊性和概率性。

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

\n","createdAt":"2025-12-18 18:16:04.664343","updatedAt":"2025-12-18 18:32:22.903885","replyToPostNumber":null,"replyCount":0,"likeCount":2,"wordCount":1502,"liked":false,"bookmarked":false,"polls":[],"reactions":[{"reaction":"❤️","count":2,"users":[{"id":182,"username":"duroy","name":"duroy"},{"id":5905,"username":"PipaQinse233","name":"PipaQinse233"}],"hasReacted":false}],"wiki":false,"version":3,"publicVersion":3,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":69058,"postNumber":2,"raw":"> **AI+ 形式化证明** 正在改变数学界的工作方式\n\n\n**陶哲轩（Terence Tao）** 有多个文章、博客帖子和演讲表达了与 Martin Kleppmann 高度相似的观点：**AI 将大幅降低形式验证（formal verification）和证明助手（如 Lean）的成本，推动其在数学和软件工程中变得主流，甚至成为标准实践**。\n\n- **关键文章与演讲**：\n - **2024 年 AMS Colloquium Lecture“Machine Assisted Proofs”**（YouTube，基于 Notices of the American Mathematical Society 文章）：系统讨论机器辅助证明历史与未来，强调 AI + 证明助手（如 Lean）可实现大规模协作、自动化验证，甚至生成完整论文 + 形式证明。预测形式化将成为常态，AI 作为“数学家的副驾驶”。\n - **博客系列（terrytao.wordpress.com）**：\n - “Formalizing the proof of PFR in Lean4 using Blueprint”（2023）：描述用 AI 辅助在 Lean 中形式化复杂证明，强调 AI 填补小缺口潜力。\n - “A slightly longer Lean 4 proof tour”（2023）：认为 AI 近期目标是自动关闭证明中的“小 sorry”（未证明部分），加速蓝图到形式证明转换。\n - “A tool to verify estimates, II: a flexible proof assistant”（2025）：开发仿 Lean 的轻量证明助手，计划集成 AI 生成伪证明后转正式 Lean 验证。\n - “Machine assisted proofs”PDF 与相关帖子：讨论 AI 与证明助手结合，验证 LLM 输出，推动形式方法普及。\n - **采访（如 Scientific American, 2024）**：AI 将成为数学家“副驾驶”，未来解释证明给 GPT，它生成 Lean 代码并验证。形式化成本将低于传统写作，推动广泛采用。\n - **其他实践**：陶哲轩亲自用 GitHub Copilot + AI 在 Lean 中形式化证明（如 PFR 猜想、Analysis I 教材），并发现手动证明中隐藏错误，证明形式验证 + AI 的实用价值。\n\n陶哲轩虽主要聚焦数学证明形式化，但其观点直接适用于软件工程：AI 生成代码 + 证明可跳过人工审查，确保正确性，与 Kleppmann“AI 生成代码需形式验证以信任”高度一致。他乐观预测这将很快成为数学（及相关领域）主流。","cooked":"

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

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

关键文章与演讲：\n
- 2024 年 AMS Colloquium Lecture“Machine Assisted Proofs”（YouTube，基于 Notices of the American Mathematical Society 文章）：系统讨论机器辅助证明历史与未来，强调 AI + 证明助手（如 Lean）可实现大规模协作、自动化验证，甚至生成完整论文 + 形式证明。预测形式化将成为常态，AI 作为“数学家的副驾驶”。
- 博客系列（terrytao.wordpress.com）：\n
  - “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 输出，推动形式方法普及。
  \n
- 采访（如 Scientific American, 2024）：AI 将成为数学家“副驾驶”，未来解释证明给 GPT，它生成 Lean 代码并验证。形式化成本将低于传统写作，推动广泛采用。
- 其他实践：陶哲轩亲自用 GitHub Copilot + AI 在 Lean 中形式化证明（如 PFR 猜想、Analysis I 教材），并发现手动证明中隐藏错误，证明形式验证 + AI 的实用价值。
\n

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

\n","createdAt":"2025-12-18 18:23:57.072767","updatedAt":"2025-12-18 19:15:26.251515","replyToPostNumber":null,"replyCount":1,"likeCount":0,"wordCount":590,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":2,"publicVersion":2,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":69059,"postNumber":3,"raw":"### 证明助手（Proof Assistant）\n\n证明助手（也叫交互式定理证明器）是一种帮助人类用计算机**严格证明**数学定理或验证软件/硬件正确性的工具。\n\n#### 核心概念\n- **形式化证明**：把数学命题和证明过程完全用精确的逻辑语言写出来，计算机能 100% 检查。\n- **证明检查器**：工具的核心部分很小（小内核原则），本身被严格验证，几乎不可能出错。即使人或 AI 写出错误证明，它也会拒绝。\n- **柯里 - 霍华德同构**：证明 ↔ 程序。写一个证明的过程就像写一个满足规格的程序（这也是很多证明助手同时支持代码生成的原因）。\n\n#### 历史关键里程碑\n- 1967 年：Automath，第一个形式化数学系统。\n- 1980 年代：Coq、Isabelle 诞生，四色定理首次被机器验证。\n- 1994 年：英特尔奔腾芯片浮点 bug 损失 4.75 亿美元，推动工业界重视形式验证。\n- 2009 年：seL4 操作系统内核被完全形式化验证（世界上第一个）。\n- 2010 年代：Lean 出现，Mathlib 数学库快速增长。\n- 2023–2025 年：AI 大爆发——DeepMind 的 AlphaProof、DeepSeek-Prover、OpenAI 等用 AI+ 证明助手解决 IMO（国际数学奥林匹克）难题，标志 AI 开始大幅降低证明成本。\n\n#### 主要应用领域\n1. **软件/硬件验证**\n - 操作系统内核（如 seL4）\n - 编译器（如 CompCert，保证编译后代码不引入 bug）\n - 密码协议、区块链智能合约、航空/医疗设备软件\n - 避免灾难性 bug（比如芯片设计错误、分布式系统一致性问题）\n2. **数学大定理证明**\n - 四色定理、开普勒猜想、费马大定理、奇数阶有限单群分类等\n - 建立大规模机器验证数学库（Lean 的 Mathlib、Isabelle 的 AFP）\n3. **编程语言设计**\n - 证明类型系统安全、并发模型正确等\n\n#### 常用工具对比（2025 年主流）\n| 工具 | 特点亮点 | 代表项目/成就 |\n|------------|---------------------------------------|----------------------------------------|\n| **Lean 4** | 速度快、自动化强、社区活跃、AI 友好 | Mathlib 最大数学库；IMO 银牌（AlphaProof）|\n| **Rocq/Coq**| 历史最久、代码生成强、小内核可靠 | CompCert 编译器、seL4 早期验证 |\n| **Isabelle**| 高阶逻辑、文档生成好、工业应用多 | seL4 完整验证、Archive of Formal Proofs |\n| **F*** | 专为程序验证 + 代码生成设计 | 安全关键软件、加密协议 |\n| **Agda** | 依赖类型纯度高，适合理论研究 | |\n| **HOL Light/HOL4** | 极简内核、数学证明强 | 开普勒猜想证明 |\n\n#### 趋势\n- **AI 与证明助手的结合**：大型语言模型（LLM）能自动生成证明草稿，证明检查器负责把关，彻底改变“写证明太贵太难”的局面。\n- 代表成果：谷歌 DeepMind、OpenAI、DeepSeek 等已在 Lean 上实现高难度数学题自动证明。\n- 未来预期：形式化证明成本大幅下降，可能像编译器一样成为软件开发的标配；数学家只需提供高层次思路，AI 填细节并验证。","cooked":"

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

主要应用领域

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

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

\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n

工具	特点亮点	代表项目/成就
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 填细节并验证。

\n","createdAt":"2025-12-18 18:26:43.682262","updatedAt":"2025-12-18 18:26:43.682262","replyToPostNumber":null,"replyCount":0,"likeCount":0,"wordCount":893,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":69060,"postNumber":4,"raw":"https://xjtu.app/t/topic/14671\n\n\n### 陶哲轩（Terence Tao）的《Analysis I》Lean 形式化项目\n\n这个 [GitHub 仓库](https://github.com/teorth/analysis) 是陶哲轩于**2025 年 5 月 31 日**正式启动的一个开源项目，目的是将他的经典实分析教材《Analysis I》（本科生水平）用**Lean 4**证明助手进行形式化翻译。\n\n#### 项目核心目标\n- **忠实复述原书**：尽可能贴近教材的定义、定理和证明结构，同时展示 Lean 的语法和特性（不追求最高效率，有时会偏离 Lean 的“习惯用法”）。\n- **作为伴侣资源**：不是取代原书，而是提供一个“带注释的伴侣”。书中留给读者的习题在这里用 `sorry`（占位符）表示，鼓励读者自己 fork 仓库填写证明。\n- **不直接引用原书文字**：只给出原书章节引用，避免版权问题。\n- **与 Mathlib 兼容**：早期章节独立定义（如第 2 章自己构建自然数），后期逐步切换到 Lean 标准数学库**Mathlib**的定义（并在章节结尾证明两者同构），这样既教学又实用。\n\n#### 技术调整（为什么与原书稍有不同）\n- 序列从**0 开始索引**（原书从 1 开始），因为 Mathlib 对ℕ（从 0 开始）的支持更好。\n- 一些原书未定义的操作（如除以 0、非 Cauchy 序列的极限）被赋“垃圾值”（如 0），确保函数是**全定义的**（total function）。Lean 对全函数支持更好，避免部分函数带来的证明复杂性（“dependent type hell”）。\n- 第 2 章自然数用归纳类型构造（而非纯公理化），但在结尾证明了 Peano 公理。\n\n#### 当前形式化进度（截至 2025 年 12 月）\n项目进展非常快，已基本覆盖全书主要内容（第 1 章引言未形式化）：\n- **第 2 章**：自然数（Peano 公理、加法、乘法）+ 与 Mathlib 同构。\n- **第 3 章**：集合论基础、函数、像与原像、笛卡尔积、基数等。\n- **第 4 章**：整数、有理数、绝对值、指数、理性数的间隙。\n- **第 5 章**：实数构造（Cauchy 序列）、序、最小上界界、实指数等 + 与 Mathlib 实数同构。\n- **第 6 章**：序列极限、扩展实数、上下极限、标准极限、子序列等。\n- **第 7 章**：级数（有限、无限、非负和、重排、根检验/比检验）。\n- **第 8 章**：无穷集合（可数、不可数、选择公理、有序集）。\n- **第 9 章**：ℝ上连续函数（子集、极限、连续性、中值定理、一致连续等）。\n- **第 10 章**：导数（基本定义、单调性、反函数导数、L'Hôpital 法则）。\n- **第 11 章**：Riemann 积分（分划、上/下积分、可积性、基本定理等）。\n- **附录 A**：数学逻辑基础（语句、蕴涵、量词、相等等）。\n- **附录 B**：十进制表示。\n\n此外，还有一些额外内容：\n- 陶哲轩的《测度论》书籍形式化（进行中）。\n- 物理单位系统形式化（包括 SI 单位）。\n- 有限选择公理（避免使用 Lean 的选择公理）。\n- 有限概率论及几个 Erdős 问题的解。\n\n#### 项目现状与影响\n- **社区活跃**：1.4k 星、181 fork、36 位贡献者，最近提交在几天前。\n- **文档网站**：https://teorth.github.io/analysis/ （每个章节有 Verso 页面、文档和 Lean 源代码）。\n- **资源**：仓库提供构建脚本、Lean 社区链接、Mathlib 搜索工具等。陶哲轩的 YouTube 频道有相关演示。\n- 这体现了陶哲轩对 AI+ 证明助手的乐观态度：项目中使用 GitHub Copilot 等工具加速形式化，正如他之前预测的，AI 正让形式验证变得更易普及。\n\n这个项目不仅是《Analysis I》的“机器可验证版本”，还是学习 Lean 和 Mathlib 的绝佳入门材料，尤其适合想结合教材和形式化证明的学生/研究者。如果你感兴趣，可以直接 clone 仓库尝试填写 sorry 部分！","cooked":"

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

项目地址:

\n\n

blog

\n\n

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 部分！

\n","createdAt":"2025-12-18 18:31:22.781423","updatedAt":"2025-12-18 18:31:22.781423","replyToPostNumber":2,"replyCount":0,"likeCount":0,"wordCount":1152,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":69061,"postNumber":5,"raw":"> **Bartosz Naskręcki**\n> Mathematician | Vice-Dean @UAM_Poznan | Researcher @ccaiwut | Rigorous mathematics, programming &ML | Passionate about what AI really understands\n\n例子：这位数学家通过 HarmonicMath 加速完成数学定理的形式化证明。\n\n---\n\n数学论文需要形式化验证。通常，这一过程由审稿人非正式地完成。但如果我们能依赖更可靠的方式，例如自动形式化为 Lean 4 代码，从而将审稿人的角色简化为对定义和定理表述进行细致检查，那会怎样？此时，自动生成代码的编译结果本身就会成为一份证明证书。这正是我与 @HarmonicMath 的 Aristotle 在一次长期运行中所实现的成果。\n\n感谢 @PietroMonticone 和 @llllvvuu 在蓝图（blueprint）搭建过程中的帮助。在此，我展示了一篇我朋友 Stefan Barańczuk 关于切比雪夫整除序列（Chebyshev divisibility sequences）论文的完整、正确的自动形式化成果。该代码包含约 5000 行高度非平凡的 Lean 代码，不仅修正了原论文中的各种不一致之处和漏洞，甚至证明了一些原本被省略的命题。\n\n相关成果可见： \nhttps://nasqret.github.io/ZsigmondyChebyshev/blueprint/index.html\n\n我将陆续发布一系列此类实验，以证明在某些数学领域——包括初等数论、组合数学和分析（即 Mathlib 所涵盖的各类内容）——我们距离大规模转变数学证明有效性的文档方式已经不远了。我认为，这一年将会非常忙碌！\n\n[grid mode=\"tile\"]\n![image|690x308](/uploads/image/54/8d/548d3d6d49a53e6efaa103eb89548cf341bfd1ce64d44fc65962ae83d3b14081.avif)\n\n![image|690x344](/uploads/image/af/6c/af6c6f6fc905fda72bc80700ff0de1c27895ebc51da74e76d83f98ce9816ab6a.avif)\n[/grid]\n\n---\n\n如果我是今天的一名学生，与最前沿的大语言模型互动几乎会让我觉得是在“作弊”。今天早上，我随手拍了一张黑板的照片，让 ChatGPT-5.2-Pro 解释其中的背景、解法，以及关于切瓦雷（Chevalley）关于可构造集（constructible sets）著名定理的一些补充评论。我收到的竟是一份极为深入的报告，它综合了来自全网的高质量代数几何材料，内容之精炼与深刻令人惊叹。\n\n这引发了一个严肃的问题：当今学生真正面对的努力与挑战究竟是什么？成本固然是一个因素，但一旦能够使用这些模型，我们该如何在这个信息丰裕的时代学习？在这个时代，解释、参考文献和交互式探索几乎都能即时获取。\n\n也许，真正的困难已不再是如何获得信息，甚至也不再是如何理解某个孤立的论证，而在于培养判断力：懂得提出什么样的问题，知道哪些解释值得信任，能够分辨深刻洞见与表面合理的区别，并将思想真正内化，而非仅仅消费内容。在一个答案唾手可得的环境中，真正的挑战或许在于如何形成品味、数学直觉，以及在知识突然泛滥的洪流中学会航行——而非沉没其中。\n\n[grid mode=\"tile\"]\n![image|690x433](/uploads/image/e4/97/e497cade3ff7cdadaf634f44f6ed6ea51d5517a276252f681f39ad26fd457756.avif)\n\n\n![image|670x500](/uploads/image/3b/8a/3b8a71f9669a9de65851803f89ab965855116ac69ed34131ede129ef89722055.avif)\n[/grid]","cooked":"

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

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

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

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

入门形式化证明

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

材料

Coq 路线

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

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

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

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

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

Mathematics in Lean — Mathematics in Lean v4.19.0 documentation

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

You are are being redirected...

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

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

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

\n","createdAt":"2025-12-18 19:03:45.069582","updatedAt":"2025-12-18 19:08:14.974024","replyToPostNumber":null,"replyCount":0,"likeCount":0,"wordCount":601,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":69064,"postNumber":8,"raw":"ETH Zurich 的数学家 Johannes Schmitt 宣布了一个重要的里程碑：OpenAI 的 GPT-5 模型首次**完全自主**地解决了一个数学领域的开放问题（open math problem），提供了完整且正确的证明，没有任何人类提示或干预。\n\n具体内容是关于枚举几何（enumerative geometry）中的一个小但新颖的贡献：涉及曲线模空间（moduli spaces of curves）上的交数（intersection numbers）。作者咨询了领域专家，确认这个问题此前是未解决的，没有明显的解法，于是提交到他参与的基准项目 IMProofBench（一个测试 AI 数学证明能力的平台）。\n\n![image|690x454](/uploads/image/9a/65/9a655d745139259b5e5806a74c0690d88326beeb84c7fb48c95ac5a8d0e7881e.avif)\n\nGPT-5 给出了一个优雅的证明，竟然绕过了该领域传统的复杂理论，而是从代数几何的另一个分支借用技术，提供了“局外人视角”的新思路。\n\n随后，他们合作撰写了一篇论文，整合了多个 AI 模型的贡献（如 GPT-5 和 Gemini 3 Pro 的证明、Claude 的写作辅助、**Lean 形式化验证**），并透明标注了每段内容的 AI/人类来源，还附上提示日志。这被视为人-AI 协作的新实验。\n\n有趣的结尾：GPT-5 在给出完美一般证明后，在一个特殊案例的示例公式上出现了幻觉（hallucination，完全编造错误内容），后来被另一个 AI（Claude）指出。\n\n![image|690x284](/uploads/image/05/f6/05f6b3ff2a3fc7fcbcac4289ccac6f0b9eb24b1c283afd463cb780f4797cfb2d.avif)\n> 幻觉示例\n\n总体来说，这个帖子标志着 AI 在高级数学研究中从“辅助工具”向“独立发现者”迈出关键一步，引发了数学和 AI 社区的广泛讨论。\n\n\nhttps://arxiv.org/abs/2512.14575","cooked":"

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

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

$\"image\"$

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

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

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

$\"image\"$

\n
幻觉示例
\n

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

\n","createdAt":"2025-12-18 19:31:34.272332","updatedAt":"2025-12-18 19:31:34.272332","replyToPostNumber":null,"replyCount":1,"likeCount":0,"wordCount":446,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":69065,"postNumber":9,"raw":"### Zulip 论坛\n\nhttps://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\n\n#### 1. **背景与数学结果**\n\n- **问题来源**：Schmitt 参与了一个叫**IMProofBench**的项目。这是一个专为测试 AI 在**研究级数学证明**能力的基准测试项目（private benchmark，避免数据污染）。项目收集了多名数学家提交的 PhD 水平开放问题。\n\n- **具体问题**：在稳定曲线模空间 $\\overline{\\mathcal{M}}_{g,n}$ 上，纯ψ类交数（descendant integrals）：\n\n$$\n\nD(\\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}\n\n$$\n\n其中 $\\sum e_i = 3g-3+n$\n（维度约束）。\n\n- **问题**：对于固定 g,n，哪些指数向量 $\\mathbf{e} = (e_1, \\dots, e_n)$ 使这个交数**最大**？\n\n- **结果**：最大值在**balanced 向量**上取得，即 $e_i$ 们尽可能均匀分布（相邻差至多 1）。最小值在集中向量（几乎所有质量在一个位置）上取得。\n\n- **证明思路**：AI（GPT-5）给出了一个简洁证明，完全绕过传统理论（如 Witten-Kontsevich 定理），只用ψ类的抽象交数性质：**nefness**（nef 类）和**Khovanskii-Teissier 不等式**（log-concavity）。\n\n- **论文**：Schmitt 迅速写成论文上传 arXiv（arXiv:2512.14575，标题《Extremal descendant integrals on moduli spaces of curves: An inequality discovered and proved in collaboration with AI》）。论文中明确标注 AI 贡献的部分（包括整段文字由 AI 撰写），并附提示日志以示透明。\n\n这是一个里程碑：这是已知第一个 AI 独立解决**研究级开放数学问题**的公开案例（此前 AI 多在竞赛题或已知问题上表现）。\n\n#### 2. **AI 的具体贡献**\n\n- GPT-5 首先生成自然语言证明（被 Schmitt 和同事验证正确）。\n\n- 其他 AI（如 Gemini 3 Pro、Claude Opus 4.5）帮助起草论文大段文字。\n\n- GPT-5.2 和 Claude Code 帮助生成 Lean 代码。\n\n- Schmitt 本人**无 Lean 经验**，一天内用 AI“vibe-coding”（随意生成 + 迭代）完成形式化。\n\n#### 3. **Lean 形式化部分**\n\n- 证明分成两部分：\n\n- **组合优化部分**（Theorem 3.1）：一个纯组合不等式，证明某些对称 log-concave 函数在 balanced 向量上取最大值。这部分被完整形式化在 Lean 中（约 3.5 页 PDF）。\n\n- **几何部分**（Theorem 3.2）：证明 descendant integrals 满足上述函数性质（用 nef + log-concavity）。这部分仍是 informal（非形式化），因为模空间本身在 Lean/mathlib 中尚未定义（这是大工程，可能需多年）。\n\n- 原始 Lean 代码：https://github.com/schmittj/balanced-vectors-blueprint\n\n- 社区成员**Eric Vergo** [快速重构代码](https://github.com/e-vergo/Balanced_Vectors)，使其更符合 mathlib 风格，并作为测试“AI 生成 Lean 证明模板”的案例。\n\n- **Kim Morrison**（Lean 专家）给出改进建议，如分离定义与证明、添加警告（定义需人工审查）。\n\n形式化好处：优化部分充满繁琐不等式，容易出错；**Lean 验证后让人放心**。Schmitt 认为这占了“50% 验证收益”，但只需“0.01% 工作量”（相比形式化整个代数几何背景）。\n\n#### 4. **社区讨论的焦点**\n\n- **惊喜与赞赏**：很多人惊叹 AI 解决开放问题、零经验下形式化 Lean（“vibe-formalizing”）。\n\n- **Kevin Buzzard**（Lean 社区大牛）指出：模空间定义本身是巨大空白（甚至椭圆曲线模空间对 Fermat 最后定理都缺），形式化几何部分可能需多年。强调 AI 不可信赖定义，但可辅助填补小 lemma。\n\n- **形式化 AI 证明的规范**：讨论如何处理 AI 生成代码的信任问题。\n\n- 建议：定义放单独文件 + 大警告，必须人工审查。\n\n- 避免 mathlib 碎片化：优先推入主库。\n\n- 讨论“quarantine”无证明义务的定义，便于审查。\n\n- **更广哲学讨论**（Timothy Chow 等）：\n\n- mathlib 是否应成“唯一正典”定义源？但数学概念往往有多个等价定义（A 类），或不等价但相关约定（B 类，如 Fourier 变换归一化）。\n\n- 形式化是否完全捕捉数学的“非形式含义”？（如“可证明性”概念的细微差别、Gödel 不完备性、数学家的“直觉”）。\n\n- Kevin Buzzard：实际论文中的定理（如 Sylow）不依赖底层基础接线。\n\n\n#### 5. **意义与启示**\n\n- **AI 在数学研究中的角色**：这例显示前沿 AI 已能发现新证明、绕过传统路径、辅助形式化。\n\n- **未来趋势**：可能出现“人+AI 混合证明”规范、专用模板处理 AI 贡献、mathlib 逐步覆盖更多代数几何。\n\n- **当前状态**（2025 年 12 月）：GPT-5 在 IMProofBench 上表现最佳（完全正确解决 22% 问题），显示 AI 已在辅助研究级数学。","cooked":"

Zulip 论坛

\n\n

1. 背景与数学结果

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

\nD(\\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}\n

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

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

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

2. AI 的具体贡献

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

3. Lean 形式化部分

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

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

4. 社区讨论的焦点

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

5. 意义与启示

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

\n","createdAt":"2025-12-18 19:40:34.19666","updatedAt":"2025-12-18 19:40:34.19666","replyToPostNumber":8,"replyCount":0,"likeCount":0,"wordCount":1254,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":69067,"postNumber":10,"raw":"充满期待，数学需要形式化验证来整治。但听说现在还比较难用。","cooked":"

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

\n","createdAt":"2025-12-19 00:56:18.309921","updatedAt":"2025-12-19 00:56:18.309921","replyToPostNumber":null,"replyCount":0,"likeCount":1,"wordCount":29,"liked":false,"bookmarked":false,"polls":[],"reactions":[{"reaction":"plus1","count":1,"users":[{"id":30,"username":"一只玉米人","name":"玉米🌽"}],"hasReacted":false},{"reaction":"❤️","count":1,"users":[{"id":30,"username":"一只玉米人","name":"玉米🌽"}],"hasReacted":false}],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":346,"username":"hoist","name":null,"avatarUrl":"/uploads/image/0d/cd/0dcdf69d213b6798002779ad4b729567cd4d889ee4a56c07a8c4454e8b563219.avif","admin":false,"moderator":false,"signatureRaw":null,"signatureCooked":null}},{"id":69076,"postNumber":11,"raw":"https://terrytao.wordpress.com/2025/12/08/the-story-of-erdos-problem-126/\n\n\n**2025 年 12 月 8 日** —— 著名数学家、菲尔兹奖得奖者陶哲轩（Terence Tao）近日在其个人博客上详述了 Erdős 问题#1026 的完整解决过程。这一源于 1975 年的经典开放问题，通过在线社区协作、人工智能工具以及既有文献的结合，最终在 2025 年 12 月得以彻底解决。\n\nErdő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 时精确达成。\n\n解决过程始于 2025 年 9 月 12 日，该问题被正式录入 Erdős 问题网站。社区成员迅速提出博弈论解读，并计算小 k 值，猜测 $c_k \\sim 2 / \\sqrt{k}$。问题一度沉寂近两个月，直至 12 月 7 日，数学家 Boris Alexeev 使用 AI 工具**Aristotle**（由 Harmonic 公司开发）对该问题进行系统扫描。\n\n![image|690x376](/uploads/image/69/46/694654e9f9fcab5a7fb84ffda9172394d02f4d3c3506757a8521b2daefbd58b4.avif)\n\n\nAristotle 在完全自主模式下，仅基于形式化陈述，成功将问题转化为矩形打包问题，并在形式化证明系统**Lean**中生成完整证明。这一成就标志着 AI 首次独立产生非平凡数学证明，并直接输出可验证的形式化代码。尽管后续人类审查发现该证明并非全新（源于 1959 年 Seidenberg 的工作变体），但 Aristotle 的自主性和效率令人瞩目——它将一个潜在的猜想直接提升为形式化定理。\n\n紧随其后，社区成员 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} $。这一链接将问题彻底闭合。\n\n陶哲轩在博客中强调：“这一解决过程融合了现有文献、在线协作与多种 AI 工具。”他指出，Aristotle 的 Lean 形式化证明、AlphaEvolve 的优化构造，以及 AI 辅助的文献检索，显著加速了进展。\n\n这一事件是 2025 年 AI 辅助数学突破的最新例证。此前，Aristotle 已独立解决多个 Erdős 问题，并在 Lean 中形式化验证。专家认为，此类工具正重塑数学研究范式：AI 擅长处理文献“暗森林”、生成形式化代码和探索数值模式，从而让人类数学家专注于核心创造性工作。\n\nErdős 问题网站维护者 Thomas Bloom 表示，该问题现已标记为“已解决”。这一协作模式或将成为未来攻克顽固开放问题的标准路径，预示着人工智能与形式化证明时代在数学领域的全面到来。","cooked":"\n

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 公司开发）对该问题进行系统扫描。

$\"image\"$

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 表示，该问题现已标记为“已解决”。这一协作模式或将成为未来攻克顽固开放问题的标准路径，预示着人工智能与形式化证明时代在数学领域的全面到来。

\n","createdAt":"2025-12-19 10:05:38.397773","updatedAt":"2025-12-19 10:07:28.367501","replyToPostNumber":null,"replyCount":0,"likeCount":0,"wordCount":928,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":69077,"postNumber":12,"raw":"其他资料\n\n- https://itp-conference.github.io/\n- https://sigplan.org/Conferences/CPP/\n- https://mathlib-initiative.org/\n- https://pitmonticone.github.io/ItaLean2025/\n- https://adam.math.hhu.de/#/\n- https://adam.math.hhu.de/#/g/emilyriehl/ReintroductionToProofs\n- Leibniz International Proceedings in Informatics\n- https://harmonic.fun/","cooked":"

其他资料

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

\n","createdAt":"2025-12-19 10:25:03.008146","updatedAt":"2025-12-19 10:25:03.008146","replyToPostNumber":null,"replyCount":0,"likeCount":1,"wordCount":24,"liked":false,"bookmarked":false,"polls":[],"reactions":[{"reaction":"💯️","count":1,"users":[{"id":30,"username":"一只玉米人","name":"玉米🌽"}],"hasReacted":false},{"reaction":"❤️","count":1,"users":[{"id":30,"username":"一只玉米人","name":"玉米🌽"}],"hasReacted":false}],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}},{"id":71075,"postNumber":13,"raw":"我们呈现了一项半自主数学发现的案例研究，使用 Gemini 系统性地评估了 Bloom 的埃尔德什问题数据库中标记为“开放”（Open）的 700 个猜想。我们采用了一种混合方法：首先通过 AI 驱动的自然语言验证来缩小搜索范围，随后由人类专家评估其正确性和新颖性。\n\n在数据库中标记为“开放”的问题中，我们处理了 13 个：其中 5 个通过看似新颖的自主解法得到解决，另外 8 个通过识别现有文献中已有的先前解法而得到处理。我们的发现表明，这些被解决问题的“开放”状态更多源于其**隐晦性**（obscurity）而非真正的难度。\n\n我们还识别并讨论了将 AI 大规模应用于数学猜想时出现的问题，特别强调了文献识别的困难，以及 AI 可能存在的“潜意识剽窃”（subconscious plagiarism）风险——即 AI 在训练中吸收了文献知识，却在输出时未适当归属或承认。\n\n最后，我们反思了 AI 辅助方法在埃尔德什问题上的经验教训与启示。\n\n---\n\n我们的结果表明，埃尔德什问题中确实存在一些“唾手可得的果实”，而当前的 AI 已经具备采摘其中一部分的能力。这为 AI 研究者提供了一种引人入胜的新型数学基准，**但我们提醒大家不要对其数学意义过度兴奋。我们在这里解决的任何开放问题，只要有合适的专家介入，其实都能相当轻松地被解决**。另一方面，人类专家的时间是有限的。AI 已经展现出加速数学发现中“注意力瓶颈”环节的潜力——前提是其可靠性能够得到显著提升。\n\n在我们的案例研究中，我们遇到了许多一开始并未预料到的困难。绝大多数在技术上正确的自主解法，其实都源自对问题陈述的错误理解或误读，而诊断这些问题有时需要付出相当大的努力。此外，对人类专家而言最困难的步骤并不是验证证明本身，而是判断该解法是否早已存在于文献之中。随着 AI 生成数学内容的增多，数学共同体必须保持警惕，防范“潜意识剽窃”现象——即 AI 在训练过程中吸收了文献知识，却在输出时未给出恰当承认和引用。请注意，形式化验证对此类问题毫无帮助。\n\n虽然在埃尔德什问题上的自主尝试取得了一些成功，但**同时也催生了误导性的炒作乃至彻头彻尾的错误信息**，这些内容随后在社交媒体平台上被进一步放大，给数学共同体带来了负面影响。除了埃尔德什问题之外，未来还会有许多其他的数学猜想与问题列表，可能成为（半）自主研究的目标。我们强烈建议此类工作认真对待本文所指出的各类问题。\n\n\nhttps://arxiv.org/abs/2601.22401","cooked":"

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

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

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

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

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

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

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

\n","createdAt":"2026-02-05 20:10:40.864645","updatedAt":"2026-02-05 20:15:08.217695","replyToPostNumber":null,"replyCount":0,"likeCount":1,"wordCount":900,"liked":false,"bookmarked":false,"polls":[],"reactions":[{"reaction":"❤️","count":1,"users":[{"id":286,"username":"TitaniumZH","name":"李嘉豪"}],"hasReacted":false}],"wiki":false,"version":2,"publicVersion":2,"deletedAt":null,"foldedAt":null,"isAnonymous":false,"isOwner":false,"user":{"id":7639,"username":"Zethes","name":null,"avatarUrl":null,"admin":false,"moderator":false,"signatureRaw":"我虽然行过死荫的幽谷，也不怕遭害，因为你与我同在。\n诗篇 23:4","signatureCooked":"

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

\n"}}],"hasMore":false,"lastReadPostNumber":1,"hasUrlPostNumber":false}