#proof assistants

据该条目，项目方宣布已在 Lean 中形式化有限单群分类（CFSG）。现有材料没有说明这次形式化覆盖了分类定理的哪些部分、依赖哪些公理，也没有给出可构建的代码或独立验证结果，因此目前应把它视为项目方公告，而非已经复核的完整证明。

Terence Tao 的幻灯片《Math 2.0》在 Hacker News 上被分享，讨论 AI 正在如何改变数学实践，涉及形式化、解释以及机器生成结果的可信度。目前可得材料是幻灯片，而非论文或可复现实验；源内容未提供，因此无法核实其中具体主张、案例或技术细节。对数学研究者、证明助手开发者和关注 AI 科研应用的人来说，这是一份用于讨论研究实践变化的材料，而不是已证实的突破。