有限单群分类定理在Lean中完成形式化

研究团队在Lean定理证明器中完成有限单群分类定理的形式化，并在过程中发现已发表证明路线中的闭包断言反例。形式化工作还促成新的群论结果及相关文献勘误。

事件进展（1 篇报道）

1. 2026-10-28 00:29
   Hacker News Classification of Finite Simple Groups Formalized in Lean

← 返回首页