AI 用 24 天、5000 万行 Lean 代码完整验证 15000 页有限单群分类定理
FuSheng_0306 · x · 2026-10-28
发帖人称 AI 在 24 天内用 5000 万行 Lean 代码，完整形式化验证了人类花半个世纪、写满 15000 页才建立起的有限单群分类定理，还修复了原著中的一个漏洞。作者据此判断 AI 智能已超越人类，并借两年前「用 GPT 写贪吃蛇被程序员嘲笑」的旧事强调范式突破会带来全面变革。核心观点：与其说 AI 不专业，不如说用户没当好审核员、没搭好 agent——用好 agent 就像用火，会用火的成了智人。
所属事件:Axiom 完成 1.5 万页有限单群分类定理的 Lean 形式化(29 条相关)→
「漫话AGI」频道最新
- Stack Overflow 月提问量跌破 1000,较 2014 峰值暴跌超 99% — DanielLockyer · 2026-10-28
- Navier-Stokes 突破已被视为常态,P vs NP 成下一个试金石 — haider1 · 2026-10-28
- Dario 姐妹淡看脑机接口,引发生人机共进化路线之争 — burny_tech · 2026-10-28
- 当购物都由 AI Agent 代理,广告业还有存在的意义吗? — VraserX · 2026-10-28
- 传闻汇总：OpenAI/Anthropic 内部模型靠游戏与模拟环境 RL 实现推理跃升 — imjustnewatai · 2026-10-28
- 逻辑学家 Jeremy Avigad：AI 之争的中心必须是我们自己 — Machine Learning Street Talk · 2026-10-28