华人AI初创完成数学史上最长证明的形式化验证，24天写出4310万行代码，全部开源

近一个月以来，AI 正逐步探入数学研究的腹地。10 月 6 日，OpenAI 在代码托管平台 GitHub 上一次性公开了 722 份由内部模型生成的数学手稿，涉及数百个开放问题；10 月 26 日，OpenAI 团队又公布了其模型在调和分析、计算复杂性理论和量子场论上的新发现。 AI 产出证明的速度越来越快，如何确认这些证明可信，就成了数学界必须面对的问题。 其中一种应对办法是形式化验证，即借助证明助手 Lean 等工具，把数学家用自然语言写成的证明逐句“翻译”成计算机能够检查的形式语言。论文中常见的“显然”“同理可得”在 Lean 里行不通，任何省略的推导和隐含的条件都必须写明，每一步推理都要经过 Lean 内核的逐条检查才算通过。 10 月 27 日，美国 AI 数学公司 Axiom 公开了一项体量罕见的成果，宣布其 AI 智能体已在 Lean 中为有限单群分类定理（CFSG）完成了完整的形式化。CFSG 的原始证明约 15,000 页，分散在 500 多篇论文中，出自约 100 位数学家之手，是人类数学史上篇幅最长的证明，人称“巨型定理”。 Axiom 的工程师和数学家调度数十个 AI 智能体，用 24 天写出约 4,310 万行 Lean 代码，目前已在 GitHub 将其开源。