7.6
深览指数
科技微博·量子位··AI 生成
陶哲轩12年前的预言，现在AI帮他兑现了
本文回溯陶哲轩如何从12年前提出AI辅助形式化数学的预言，到亲自下场学习Lean证明系统，并最终通过PFR、Equational Theories等项目，用「AI辅助证明+Lean自动验证+志愿者协作」的模式，48小时内攻克2200万个代数关系。核心信息是：陶哲轩不是坐等预言成真，而是通过实际行动和项目推动，把预言变成现实。适合对AI在科研中的应用、形式化数学感兴趣的深度读者。原文 ↗
核心观点
- ▍陶哲轩12年前在首届数学突破奖上提出的三个预言——大规模数学协作、计算机自动验证证明、形式化语言取代LaTeX——正在通过AI和Lean系统成为现实。
- ▍最好的预言家是先行者：陶哲轩不止预判未来，还亲自下场学习Lean、发起PFR和Equational Theories等项目，用行动把设想变为现实。
- 012013年陶哲轩提出预言时，Transformer和ChatGPT尚未诞生，该预言在当时被视为天方夜谭。
- 022023年10月，48岁的陶哲轩决定正式学习Lean4交互式证明系统，原计划1周完成的麦克劳林不等式形式化证明，实际耗时1个月才完成。
- 032023年11月，陶哲轩与合作者完成PFR猜想论文后，将其拆解为子任务开放社区，使用Lean进行自动核验，全程仅3周完成所有形式化工作。
- 042024年9月，陶哲轩发起Equational Theories项目，针对约2200万个代数等式，采用「AI写证明+Lean验证+志愿者协作」模式，48小时内完成大规模筛选，前9天进度达99.866%。
- 05该项目还催生了新的数学概念magma cohomology（原群上同调），用于分类原群扩张、构造反例。
- 06陶哲轩2岁教比自己大的孩子数数，10岁成IMO最年轻铜牌得主，24岁成UCLA最年轻终身教授之一，31岁获菲尔兹奖。
- 072009年陶哲轩参与Polymath项目，证明了大规模协作在数学上可行，但也发现人工验证速度跟不上协作规模的核心瓶颈。
- 08陶哲轩认为，未来数学家的核心竞争力在于与AI协作的能力，并建议年轻学者掌握这一技能。
反方 / 局限
- — 文章提及陶哲轩学习Lean初期碰壁，发现形式化证明与写传统数学论文是两种完全不同的思维模式，原本‘显然’的步骤需要补充大量形式化细节，单行推导可能变成数百行代码。
陶哲轩LeanPolymath项目PFR猜想Equational TheoriesMagma CohomologyKevin BuzzardBen GreenTim Gowers麦克劳林不等式LaTeXOpenAIDeepMindUCLA数学突破奖
7 分钟 · 4 卡片 · 7 资料
读原文 →