菲尔兹奖得主十年前预言形式化语言将取代LaTeX，如今通过Equational Theories项目借助AI在48小时内攻克多数难题，展现人机协作新范式。
菲尔兹奖获得者陶哲轩曾在12年前提出数学研究将转向计算机可理解的形式化语言，而非传统LaTeX排版。这一预言近期随着人工智能技术的发展得到验证。过去一年间，AI在数学证明领域取得显著进展，包括OpenAI解决开放性问题以及DeepMind批量攻克数学猜想。陶哲轩作为早期实践者，通过推进大规模协作数学项目、Lean形式化证明系统以及发起Equational Theories计划，实现了将形式化语言与人工智能结合的实际应用。
在Equational Theories项目中，研究团队面对2200万个数学问题，采用人类专家与AI协同工作模式，仅用48小时便解决其中大部分。该系统运行效率极高，许多情况下无需陶哲轩本人直接介入即可完成验证任务。这一成果标志着数学证明流程的自动化程度达到新高度，同时也体现了形式化方法在大规模数学问题处理中的可行性。
陶哲轩的职业生涯始终以协作创新为核心特征。早在2009年他便参与Polymath项目，尝试将开源协作模式引入数学研究。其个人履历包括10岁获国际数学奥林匹克铜牌、24岁任加州大学洛杉矶分校最年轻终身教授之一以及31岁荣获菲尔兹奖。当前AI与形式化证明的结合不仅实现了他多年前提出的设想，也为未来数学研究提供了可复制的技术路径。该技术路线可能改变传统学术出版与验证机制，推动数学领域向更透明、可重复的方向发展。