华人团队完成史上最长数学证明的形式化验证，开源4300万行代码

近日，人工智能逐渐深入数学研究领域。10月6日，OpenAI在GitHub上发布了722份由其内部模型生成的数学文稿，涵盖数百个未解决的问题。随后在10月26日，OpenAI团队又分享了在调和分析、计算复杂性理论和量子场论方面的新发现。随着AI生成数学证明的速度加快，验证这些证明的可信性成为数学界面临的重要挑战。目前，一种有效的解决方案是形式化验证，即利用证明助手如Lean等工具，将数学家以自然语言书写的证明逐步“翻译”为可供计算机审核的形式语言。在这一过程中，常见的简化表达如“显然”或“同理可得”均无效，所有推导和条件必须详尽列出，每一步推理也需经过Lean内核的细致检验。

在此背景下，10月27日，美国AI数学公司Axiom宣布其AI系统在Lean中完成了有限单群分类定理（CFSG）的完整形式化，这一成果规模庞大。CFSG的原始证明确实为人类数学史上最长，约15,000页，分布于500多篇论文，由约100位数学家合作完成，被称为“巨型定理”。Axiom的团队在24天内调配数十个AI智能体，共编写了约4,310万行Lean代码，并已将其开源至GitHub。