Axiom宣布完成有限单群分类定理形式化
热点事件持续更新
Axiom宣布完成有限单群分类定理形式化
1 篇报道1 个报道来源6 小时前更新
先了解这件事
AI 综述
Axiom Math宣布，数十个 AI Agent 在数学家和工程师组织下，用 24 天完成有限单群分类定理的 Lean 形式化，给出了覆盖整个定理的计算机检查证明。工程把分散在 500 多篇论文中的推理组织成形式系统，生成约 4310 万行代码和 205 万个形式化声明。 Axiom 还称，Agent 在过程中发现一处存在近 40 年的历史论证漏洞，并参与构造一项新的群论结果。
AI 根据报道生成 · 46 分钟前更新
最新进展10月28日 14:37
Axiom Math 数十个 AI Agent 用 24 天形式化有限单群分类定理并发现近 40 年的漏洞报道时间线
沿着报道，了解事件的不同侧面。
10月28日
- 知乎专栏：机器之心精选Axiom Math 数十个 AI Agent 用 24 天形式化有限单群分类定理并发现近 40 年的漏洞
Axiom Math 宣布，数十个 AI Agent 在 24 天内完成有限单群分类定理的 Lean 形式化，生成约 4310 万行代码和 205 万个形式化声明，并给出覆盖整个分类定理的计算机检查证明。工程将分散在 500 多篇论文中的推理组织成可逐步检查的形式系统。过程中，Agent 还发现一处存在近 40 年的历史论证漏洞，并参与构造一项新的群论结果。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。