华人AI初创24天完成史上最长数学证明形式化验证并开源

随着AI批量生成数学证明，如何确认其可信度成为数学界难题。10月27日，美国AI数学公司Axiom宣布，其AI智能体已在Lean证明助手中完成有限单群分类定理（CFSG）的完整形式化，并在GitHub开源。该工程在24天内由数十个智能体协同完成，生成约4310万行代码，形成数学史上最长证明的机器可检验版本。 CFSG被称为“巨型定理”，原始证明约1.5万页、分散在500多篇论文中，由约100位数学家历经数十年完成，涉及大量记号差异与隐含前提，完整核验长期困难。Axiom团队将论证拆解为108个里程碑和约380项子任务，借助Lean社区数学库及清华求真书院等积累代码推进。过程中，智能体曾因误设前提删除数万行代码，团队也通过拆分任务、建立缓存系统解决验证瓶颈。10月26日，Lean内核确认从公理到定理的全部推导通过检查。 Axiom由洪乐潼创立，她与创始数学家小野健等提出“形式化验证一切”。该公司称，形式化不仅验证CFSG，也发现笔误、数据错误和遗漏条件，并指出与已发表文献存在34处偏差。其中非平衡群定理一处关键论证出现反例，团队在莱昂斯与所罗门等学者帮助下另寻路线并完成证明。该成果为AI辅助数学提供可复核样本，或使未来机器证明从依赖同行信任转向可运行、可追溯的公共检验。