菲尔兹奖得主陶哲轩：如何利用 AI 与 Lean 开启数学研究的新范式

菲尔兹奖得主陶哲轩正积极倡导利用人工智能重塑数学研究，标志着该领域正经历一场深刻的范式转移。文章详细记录了他从 2022 年开始接触交互式证明系统 Lean，到主导 PFR 猜想的形式化证明，再到启动“Equational Theories”大规模实验项目的历程。在 PFR 项目中，陶哲轩展示了如何利用 Lean 将复杂证明分解为模块化子任务，通过全球志愿者协作并由机器自动校验，有效解决了传统大规模数学协作中的验证瓶颈。随后，他进一步尝试结合 Python 脚本、自动定理证明器以及大语言模型，对涉及 4600 多个代数定律和 2200 万种逻辑蕴涵的庞大问题进行系统性筛查。陶哲轩指出，虽然目前的 LLM 行为类似“过度自信的本科生”，但在处理大量琐碎子问题和形式化代码转换上极具潜力。他认为，这种结合人类直觉、AI 辅助与形式化验证的方法，正在将数学从个人的理论推导转变为类似物理学大型实验的“实验数学”，为未来的科研协作提供了新的蓝图。

事件分析

💡 核心观点：陶哲轩利用 Lean 与大模型将数学研究转变为“实验科学”，证明了 AI 是拓展人类认知边界的协作工具而非替代品。