陶哲轩12年前的预言，现在AI帮他兑现了

2026-06-20 20:21:47

数据炼金师

发布在

快讯

阅读：1174

12年前，菲尔兹奖得主陶哲轩曾预言：未来数学论文将使用计算机理解的形式化语言，并实现自动验证与大规模协作。如今，他正借助AI亲手兑现这一预言。自2023年起，陶哲轩学习Lean4证明系统，发起PFR猜想形式化项目，仅三周即完成验证。2024年9月，他发起Equational Theories项目，面对2200万个代数等式，通过“AI+Lean+全球社区”协作，48小时内攻克大半，更催生出全新数学概念。陶哲轩用行动证明，AI与人类协作正极大提升数学研究效率，他已成为AI数学最坚定的布道者。

原文链接

本文链接：https://kx.umi6.com/article/36624.html

转载请注明文章出处