形式化费马大定理

原文 ↗ Hacker News 讨论 ↗

一个 AI 系统在 11 天内生成了费马大定理的完整 Lean 形式化，为现代数学最著名的结果之一产出了 1300 万行机器检查的证明代码。评论者将其视为自动定理证明和形式化方法的一个里程碑，但也提出了关于验证可信度（证明助手可能存在 bug）、证明可读性，以及这种海量 AI 生成的形式化是否能被人类复用或是否有意义的担忧。讨论还延伸到更广泛的影响：大规模 AI 推理的成本与效率、它对数学职业和研究经费的影响，以及未来系统是否可能从形式化已知证明走向发现根本上新的证明。

结果的性质

  • 讨论强调，这不是费马大定理（FLT）的一个新的数学证明，而是对现有 Wiles/Taylor 风格证明的 Lean 形式化。
  • 若干评论者指出，数学界早已基本认为 FLT 已经尘埃落定；新意在于 autoformalization 的规模和速度。
  • 该形式化遵循的是 1990 年代的一种阐述，而不是最新、最精简的做法，并处理素数 ≥17；其他先前的形式化覆盖了剩余情况。

规模、成本与工具链

  • Claude 在约 11 天内生成了约 1300 万行 Lean 代码和约 2.95 万个引理，使用了约 60 亿输出 token 以及大量算力（数百 GB 内存、许多核心）。
  • 按公开 API 价格粗略估算，成本大约在数十万美元量级，但也有人争论内部推理是否便宜得多，以及训练成本应如何摊销。
  • 一个协作式 Lean 平台（prove2.me）和自定义编排（“swarm of agents”）是关键；一些人将此视为结构化工具对严肃工作至关重要的证据。

信任、正确性与 Lean 内核

  • 许多人会问：1300 万行代码如何值得信任？回应是：Lean 的类型检查器会验证每一步；人类主要需要信任：
    • FLT 的形式化陈述，
    • 小型内核和公理，
    • 以及一个二级检查器（“comparator”），用于重新验证最终定理。
  • 也有人提醒，Lean 最近出现过健全性 bug，包括一个由 AI 找到的、利用内核 bug 的 Collatz“反证”；多个独立检查器可以降低风险，但不能完全消除。
  • 有人希望将其翻译到其他系统（例如 HOL/Metamath）以获得额外保证。

对数学的价值与复用

  • 支持者认为：大型证明工作通常会产生许多可复用的抽象；autoformalization 可以发现文献错误并减轻审稿负担。
  • 怀疑者认为：1300 万行可能只是“AI slop”，抽象质量差，难以整合进标准库；也未必提升人类理解。
  • 一个仍在进行中的人类 FLT 形式化项目有不同目标：贡献干净、通用的 mathlib 组件，以及一个人类可探索的“动态文档”。

对数学家与职业的影响

  • 情绪复杂：既为能力感到震撼，也担心初级研究者会被 LLM “抢跑”。
  • 有人认为，形式化与发现证明并不相同，因此人类在创造力和表述上仍有巨大空间。

更广泛的 AI 影响与伦理

  • 乐观者认为，这表明 AI 能处理数学中的大块领域，并可类比到科学问题（例如医学、物理）。
  • 悲观者担心权力集中、算力预算不透明、为 IPO 制造炒作，以及最强模型的公众可访问性有限。
  • 讨论中还出现关于人类意义、“扮演上帝”（例如治愈衰老）以及 AI 进步是改善还是削弱人类福祉的哲学争论。

未来方向

  • 建议的下一个目标包括：有限单群分类、黎曼猜想、P vs NP。
  • 还有几位希望后续 AI 再次处理时，能对 FLT 形式化进行彻底简化和重构，或者从某种形式意义上证明它已经接近最小。