Lean 4 形式化证明：每个有限单群都可由两个元素生成
geoffreyirving · x · 2026-11-03
AxiomMath 项目发布了一个 Lean 4 证明仓库 CFSGCorollary，证明了「每个有限单群都由两个元素生成」这一定理。该证明基于同一项目的 CFSG（有限单群分类定理）形式化，依赖 TauCeti 的 ClassificationStatement 陈述——即每个有限单群同构于 TauCeti 列表中的某一个群。仓库包含条件性与无条件性两个定理版本，采用 Apache-2.0 许可证。这是数学大定理形式化验证的一个具体推进。
「研究」频道最新
- EAT 进化智能体团队:内核优化任务刷新 SOTA,Open Kernel Challenge 排名第4 — berkeley_ai · 2026-11-03
- 声称 GPT-6 Astra 直接编辑 Qwen 权重，MATH-500 从 7.9% 提至 48.1% — 1-800-methdyke · 2026-11-03
- 研究者批「权重空间编程」：Atari 是送答案的选择题，Qwen 案例近乎喂答案 — anshulkundaje · 2026-11-03
- Cohere 论文：相邻 token 共享 20-45% 专家，MoE 投机解码低批量也划算 — rohanpaul_ai · 2026-11-03
- 直接改 13.1 万个权重：研究者用激活定向修复模型循环推理 — xennygrimmato_ · 2026-11-03
- 拆分注意力≠拆分上下文：多 agent 审阅文档的隐藏陷阱 — krishnan · 2026-11-03