人类历史上最宏大的数学成就——有限单群分类定理（CFSG），如今已完全通过计算机形式化验证。这一由百余名顶尖数学家耗时半个多世纪、撰写长达15000页的“数学天书”，被初创团队Axiom开发的多智能体AI系统在短短24天内彻底解析并验证完毕。
更令人震撼的是，AI为此构建了人类史上首个超过4000万行的Lean代码库。按代码行数计算，该项目已成为史上最大的开源软件，规模远超Linux内核、Chromium、Firefox、LLVM、GCC及FFmpeg等知名项目。值得注意的是，AI不仅完成了验证，还发现了原证明中的人类疏漏，并通过自主推导新的数学定理填补了这些漏洞。
著名数学家Ken Ono在见证这一历史时刻时激动落泪。他回忆起童年时父亲引导自己接触群论大师的经历，感慨人机协作终于跨越了这一数学界的终极门槛。然而，这一突破也引发了复杂的情绪：部分研究者因成果被AI“抢先”而焦虑，另一些人则担忧纯粹“发现之乐”的消逝。这些泪水背后，折射出数学界在AI时代对自身角色与价值的深层反思。