Hopf 问题百页证明数日内被 Codex 形式化 25 万行 Lean

games-and-games · reddit · 2026-08-28

数学圈出现惊人进展：Levent Alpöge 发布了一份据称约 100 页、与 Claude 协作写成的证明，宣称解决了悬置 78 年的 Hopf 问题。仅两天后，OpenAI 的 Boris Alexeev 用 Codex 将该证明形式化为约 25 万行 Lean 代码，初步看检查通过。作者感叹：此刻可能没有任何一个人能完全理解证明的全部细节——AI 辅助的数学证明与形式化验证速度已超出人类个体的消化能力。