陶哲轩12年前预言成真：AI助力形式化数学证明，48小时攻克2200万问题
2026/06/20 19:56阅读量 71
菲尔兹奖得主陶哲轩在2014年预言数学家将使用形式化语言替代LaTeX、计算机自动验证证明。12年后，他通过Lean形式化系统、PFR猜想证明和Equational Theories项目，用AI+人类协作模式实现预言：48小时内处理约2200万个代数蕴含关系，证明大规模协作数学可行。
事件概述
菲尔兹奖得主陶哲轩12年前在首届数学突破奖上预言，数学家未来将不再用LaTeX撰写论文，而是使用计算机能理解的形式化语言。如今，随着AI在数学领域提速，从OpenAI解决开放问题到DeepMind批量攻克数学猜想，这一预言逐渐兑现。陶哲轩本人亲自下场，通过Lean形式化证明系统、PFR项目和Equational Theories项目，展示了AI+人类协作如何将数学研究效率提升至新高度。
核心信息
- 预言背景：2014年，陶哲轩提出三个预言：大规模数学协作成为常态；计算机自动验证数学证明；LaTeX被形式化语言取代。当时Transformer和ChatGPT尚未出现。
- 关键工具与项目：
- Lean形式化系统：交互式定理证明系统，可逐行验证数学证明逻辑。2023年10月，48岁的陶哲轩开始学习Lean4，并用约一个月完成首个形式化证明（麦克劳林不等式）。
- PFR猜想项目：2023年11月，陶哲轩与合作者完成PFR猜想论文后，启动Lean4形式化项目，将论文拆解为子任务开放给全球社区。系统自动核验，全程仅三周完成所有形式化工作。
- Equational Theories项目：2024年9月25日发起，目标是确定约2200万个代数等式之间的逻辑蕴含关系。采用AI辅助写证明、Lean负责检查、志愿者社区分头攻坚的协作模式。48小时内完成大规模筛选，前9天进度达99.866%，第57天主项目基本完工，仅剩162个蕴含关系待收尾。
- 新概念诞生：项目过程中催生了“magma cohomology（原群上同调）”，一种为无公理约束的原群量身打造的上同调理论。
值得关注
陶哲轩的经历表明，AI与形式化验证的结合正在改变数学研究范式。从Polymath项目（2009年证明大规模协作可行但受限于人工审核）到Lean自动核验彻底解除验证瓶颈，再到Equational Theories项目中AI直接参与证明写作，陶哲轩一步步将曾经的设想变为现实。他已成为AI数学最坚定的布道者，并建议年轻学者掌握与AI协作的能力。