熱點事件持續更新
Axiom Math發佈有限單羣分類形式化證明
1 篇報道1 個報道來源1 小時前更新
先了解這件事
AI 綜述
2026年10月28日，Axiom Math 發佈其稱為首個完整經電腦核查的有限單羣分類證明。報道指，整個形式化工作歷時24日，包含約43.1M行Lean程式碼，由工程師和數學家指揮數十個AI Agent完成；Lean kernel 核查了每一步邏輯。形式化過程亦揭出已刊文獻中34項值得注意的偏差。Axiom表示，正與羣論學者整理勘誤，以處理形式化過程揭出的偏差。
AI 根據報道生成 · 1 小時前更新
最新進展10月28日 01:10
Axiom Math 發佈其稱首個完整經電腦核查的有限單羣分類證明。報道時間線
沿着報道，瞭解事件的不同側面。
10月28日
- Unite.AI精選Axiom Math 發佈 43.1M 行 Lean 有限單羣分類證明
Axiom Math 發佈其稱為首個完整經電腦核查的有限單羣分類證明，歷時 24 日並包含約 43.1M 行 Lean 程式碼。工程師和數學家指揮數十個 AI Agent 完成形式化，Lean kernel 核查每一步邏輯。形式化過程揭出已刊文獻中 34 項值得注意的偏差，Axiom 表示正與羣論學者整理勘誤。
本事件熱度走勢
還沒有足夠的連續觀測數據，暫不繪製趨勢。