Axiom称完成有限单群分类定理形式化
热点事件历史事件
Axiom称完成有限单群分类定理形式化
1 篇报道1 个报道来源4 天前更新
先了解这件事
AI 综述
Axiom称，其多智能体系统AxiomProver用24天完成有限单群分类定理的形式化验证，生成4310万行Lean代码，并构建了规模最大的Lean代码库。报道还称，系统发现原证明存在34处重大逻辑偏差，并指出“不平衡群定理”的漏洞；AxiomProver随后证明新定理，补上关键缺口。
AI 根据报道生成 · 1 小时前更新
最新进展10月30日 19:57
Axiom多智能体系统24天形式化验证有限单群分类定理报道时间线
沿着报道，了解事件的不同侧面。
10月30日
- 腾讯新闻Axiom多智能体系统24天形式化验证有限单群分类定理
Axiom的多智能体系统AxiomProver用24天将有限单群分类定理形式化，产出4310万行Lean代码，并构建出规模最大的Lean代码库。形式化过程中，AI发现原证明存在34处重大逻辑偏差，并以反例指出不平衡群定理中的漏洞；AxiomProver随后证明新定理，补上关键缺口。