Kevin Buzzard 提 PR 证明单位球是黎曼流形，引发 Lean 数学库现状争论
JasonRute · x · 2026-10-19
Jason Rute 发帖质疑：为何 Kevin Buzzard 9 月 26 日还在向 mathlib 提交「单位球面是黎曼流形」的 PR,而 9 月 28 日就出现了 Ricci flow 的完整形式化？他自答：一个是 mathlib,一个是「vibe coded(AI 随手生成)」，甚至分不清先后。
由此引发一场关于 Lean 形式化数学现状的讨论：
- eigenstate 追问：我们到底有没有一个可用的微分几何 Lean 库？哪些工作流真正可行？能否快速形式化研究中的微分几何命题并确信写的就是所想？
- jacobaustin132 认为 Tau Ceti 库补上了 mathlib 缺的一部分，但 AI 自己「vibe 出基础库」的速度可能比 mathlib 或 Tau Ceti 的演进更快；他预计爱好者会向 Prove2Me、Tau Ceti 等自动化证明项目大量投入 Claude tokens,三个月内主要结果就能形式化完毕，之后 AI 直接复用这些现成仓库即可。
- 双方还辩论了「是否需要理解 AI 到底证明了什么」：eigenstate 担心只靠 vibe 直觉会信任错误的证明，jacobaustin132 则相信足够聪明的 AI 不会证明错。
「研究」频道最新
- IFM 开源 RL360:8192 并发沙箱、130 万 rollouts 的 RL 基建 — rupspace · 2026-10-23
- 号称匹敌 GPT-6.1 的 DNA 模型遭实测打脸：10 例 8 例不如随机 — anshulkundaje · 2026-10-23
- AI 揭穿阴谋论研究风波落幕：Science 撤回关注声明，结论不变 — DG_Rand · 2026-10-23
- Embodied First Exam：一行代码在 44 台机器人上考你的 Agent — ManlingLi_ · 2026-10-23
- Anima Anandkumar 演讲：AI 气象模型胜超算，但不会取代科学家 — AnimaAnandkumar · 2026-10-23
- GLM-5.3-Flash 实现 1M token 上下文训练，较基线提升 64 倍 — AndrewLBeam · 2026-10-23