Lobsters | 📄 原文链接 | 2026-07-22 collected

人类数学家正在被反例碾压：AI 形式化数学的时代来临

source: xenaproject.wordpress.com — 2026-07-20

概述

本文回顾了过去两个月在数学形式化领域的剧变。2026 年 5 月 20 日，ChatGPT 推翻了 Erdos 单位距离猜想；一周内 Logical Intelligence 用 Lean 形式化了整篇 AI 生成的论文；6 月 26 日 OpenAI 的 Sol 模型在 3 周内生成了 120 万行 Lean 代码，完全形式化了该猜想的反例证明，包含 100+ 页的全局类域论。整个 mathlib 花 9 年达到 230 万行，而 Sol 用 3 周就接近其一半。作者（Xena Project 创始人）坦言：AI 大规模生成数学证明已不可避免。

核心要点

  • 2026 年 5 月 20 日，ChatGPT 推翻了 Erdos 单位距离猜想，在离散几何领域找到了反例。
  • OpenAI 的 Sol 模型在 3 周内生成了 120 万行 Lean 代码，完整形式化了该猜想的证明——包括曾被认为遥不可及的全局类域论。
  • Lean 的核心数学库 mathlib 耗时 9 年达到 230 万行，AI 用 3 周完成了接近一半的规模。
  • 多个 AI 公司（Logical Intelligence、Logos、Harmonic、Axiom AI）都在开发 自动形式化工具，将人类数学语言翻译为 Lean。
  • 关键转折点：形式化研讨会中，Claude Max 在 10 分钟内形式化了一个 有限群方案的 Oort 猜想反例，而人类数学家花了三周验证原始论文。

金句

It was at this point that the penny really dropped for me — large AI-generated developments of mathematics are inevitable.
back to Lobsters