本文回顾陶哲轩从 12 年前预言到亲自下场，通过 Lean 形式化证明与 AI 协作，将大规模数学协作从设想变为现实的历程。
📝 详细摘要
文章以陶哲轩 2014 年关于「形式化语言取代 LaTeX」的预言为引，梳理了他从 Polymath 项目到 Lean 形式化证明、再到 Equational Theories 项目的十年实践。重点讲述了陶哲轩如何从「天才独行侠」转变为协作数学的推动者，以及他如何借助 Lean 系统解决协作验证瓶颈，最终在 PFR 猜想和 2200 万个代数等式项目中，通过「AI + 人类 + Lean」三方协作，实现 48 小时攻克大半问题的效率突破。文章也提及项目过程中催生的新数学概念「magma cohomology」，并点明陶哲轩已成为 AI 数学最坚定的布道者。
💡 主要观点
- 陶哲轩 12 年前预言的形式化数学，如今通过 AI 与 Lean 系统成为现实。 2014 年他提出用机器可读的形式化语言取代 LaTeX，当时被视为天方夜谭；如今 Lean 系统与 AI 辅助已能自动验证数学证明，预言被兑现。
💬 文章金句
- 将来有一天，我们或许不再用 LaTeX 撰写论文，而是使用计算机能理解的形式化语言。
- 最好的预测未来，就是亲手把它创造出来。
- 数学家能不能像开源软件开发者一样协作？
📊 文章信息
AI 初评：86
来源：量子位
作者：闻乐
分类：人工智能
语言：中文
阅读时间：12 分钟
字数：2781
标签： AI 数学, 形式化证明, Lean, AI 协作, 陶哲轩