陶哲轩12年前预言被AI兑现
速览
全球知名数学家陶哲轩近期展现出对人工智能技术的极度热情，成为AI领域的狂热布道者。他曾在12年前提出某些数学难题或猜想，如今这些挑战正通过AI辅助得以解决或验证。这一现象标志着AI在复杂逻辑推理和科学发现领域取得了突破性进展，也体现了顶尖科学家对AI潜力的认可。
AI 深度解读
背景
菲尔兹奖得主、被誉为“全球最聪明的人之一”的陶哲轩（Terry Tao），在12年前首届数学突破奖（Breakthrough Prize）的演讲中抛出了一个在当时看来近乎“天方夜谭”的预言。彼时，Transformer 架构尚未诞生，ChatGPT 更是无影无踪，数学界的主流范式仍依赖于传统的 LaTeX 撰写论文以及人工推导证明。
陶哲轩预言，未来数学家将不再单纯依赖 LaTeX，而是转向使用计算机能理解的“形式化语言”；计算机将具备自动验证数学证明的能力；大规模的人类协作将成为数学研究常态。这一预言曾被视为过于超前，但随着过去一年来 AI 在数学领域的爆发式进展，这一预言正被逐步兑现。陶哲轩本人也从预言者转变为坚定的实践者和布道者，通过 Lean 形式化证明系统和 AI 协作，亲自验证并推动了这一变革。
核心内容
陶哲轩的职业生涯始终贯穿着对“数学协作”的探索。早在 2009 年，他参与了 Polymath 项目，尝试将数学协作搬上公开论坛，证明了大规模协作在解决组合数学问题上的可行性。然而，他敏锐地发现了该模式的瓶颈：随着参与者增多，人工审核和纠错的压力呈指数级增长，缺乏自动验证工具使得协作规模难以突破天花板。
为解决这一痛点，陶哲轩在 2014 年提出了包含三个核心维度的未来数学愿景：大规模协作常态化、计算机自动验证证明、以及形式化语言取代 LaTeX。
转机出现在 2023 年。陶哲轩结识了 Lean 交互式定理证明系统的早期推广者 Kevin Buzzard。Lean 允许用形式化语言描述数学证明，并由计算机逐行验证逻辑。尽管陶哲轩起初低估了形式化证明的难度——他试图将麦克劳林不等式的传统证明转译为 Lean 代码，却因形式化语言要求极高的严谨性（如明确引用引理、补全所有隐含细节）而碰壁，耗时一个月才完成首个正式化证明，但他由此正式融入了形式化数学社区。
随后，陶哲轩将这一理念应用于实际研究。在 2023 年 11 月，他与 Ben Green、Tim Gowers 等人完成关于 PFR 猜想（集合加法结构数论命题）的论文后，立即启动 Lean 形式化项目。不同于 Polymath 的人工审核，该项目利用 Lean 进行自动审查，全球社区成员认领子任务，系统自动核验。仅用三周，所有形式化工作即告完成，验证了自动化协作的高效性。
2024 年 9 月 25 日，陶哲轩发起了规模更大的 Equational Theories 项目，旨在确定约 2200 万个代数等式之间的逻辑蕴含关系。该项目采用了“AI 辅助生成证明 + Lean 自动验证 + 全球志愿者社区攻坚”的混合模式。结果惊人：48 小时内完成大规模筛选，第 9 天进度达 99.866%，第 57 天主项目基本完工。此外，该项目还意外催生了新的数学概念“magma cohomology”（原群上同调），用于研究最一般的代数结构。
关键要点
- 预言的兑现：陶哲轩 12 年前关于“形式化语言取代 LaTeX”、“计算机自动验证证明”及“大规模协作常态化”的预言，在 AI 技术成熟的背景下已初步实现。
- 技术基石 Lean：Lean 交互式定理证明系统是连接人类数学直觉与机器自动验证的关键工具，它要求证明过程具备机器可读的极高严谨性，解决了大规模协作中的信任与审核难题。
- 协作模式的迭代：
- Polymath 阶段：依赖公开论坛和人工审核，受限于组织成本和纠错效率。
- PFR 猜想阶段：引入 Lean 自动审查，实现子任务独立认领与自动合并，效率大幅提升。
- Equational Theories 阶段：形成“AI 生成 + Lean 验证 + 人类社区”的三方协同闭环，具备高度自主运转能力。
- AI 与数学的深度融合：AI 不再仅仅是辅助工具，而是深度嵌入研究流程。在 Equational Theories 项目中，AI 负责初步证明生成，Lean 负责逻辑校验，人类负责复杂难题攻关，这种分工使得陶哲轩本人无需全程介入即可推进项目。
- 新数学概念的诞生：自动化大规模计算与验证不仅提高了效率，还意外发现了新的数学结构，如为无公理约束的原群量身打造的“magma cohomology”理论。
意义与影响
陶哲轩的实践标志着数学研究范式的一次重大转型。首先，它证明了形式化数学不再是理论构想，而是可操作、高效率的研究手段。通过 Lean 等工具，数学证明的严谨性得到了机器级别的保障，极大地降低了协作中的沟通成本和错误率。
其次，这一模式展示了人机协作在基础科学研究中的巨大潜力。AI 处理海量数据的筛选与初步推导，人类专注于创造性思维与复杂逻辑构建，两者互补使得解决如 2200 万个等式关系这类超大规模问题的成为可能。
最后，陶哲轩作为顶级数学家的亲身下场，极大地推动了AI 数学社区的发展。他不仅是预言者，更是先行者，通过公开项目鼓励年轻学者掌握与 AI 协作的能力。这种从“天才独行侠”到“协作布道者”的转变，预示着未来数学研究将更加开放、透明且高效，为其他科学领域提供了可借鉴的协作范式。