05:39
0
AI在24天内完成4000万行CFSG形式化证明
据格隆汇报道,10月31日,Axiom的多智能体AI系统完成了对有限单群分类(CFSG)的形式化验证,这是人类最大的数学证明。这项验证耗时一个多世纪,由全球100多位顶尖数学家撰写,篇幅超过15,000页,而AI系统仅用24天就全部处理完成。这一努力生成了一个超过4000万行的Lean代码库,按代码行数计算,现已成为最大的开源软件项目,超过了Linux内核、Chromium、Firefox、LLVM、GCC和FFmpeg。AI系统还识别出原有人工证明中的漏洞,并提供了新的数学定理来完成修正。