AI 颠覆数学研究！陶哲轩借 AI 破解数学猜想，形式化成功惊呆数学圈

图片地址：https://img.ithome.com/newsuploadfiles/2023/12/376cd073-ae61-41f7-b5f2-202044452b3c.jpg?x-bce-process=image/format,f_auto

【新智元导读】历时三周，陶哲轩成功地用 AI 工具完成了形式化多项式 Freiman-Ruzsa 猜想证明过程的工作。他再次呼吁数学研究者学会正确利用 AI 工具，网友惊呼：以后的数学论文不需要人类可读了？用 AI 工具辅助研究数学的项目，再一次被陶哲轩跑通！三周前，他曾发布一篇博文，记录下自己使用 Blueprint 在 Lean4 中形式化多项式 Freiman-Ruzsa 猜想的证明过程。就在昨天，他激动宣布：将多项式 Freiman-Ruzsa 猜想的证明形式化的 Lean4 项目，在三周后取得了成功！现在，依赖关系图已经完全被绿色所覆盖，Lean 编译器也报告说，这个猜想完全遵循标准公理。陶哲轩表示，在整个团队中，自己贡献的代码大概只有 5%。这个结果很鼓舞人心，因为这意味着数学家即使不具备 Lean 编程技能，也能领导 Lean 的形式化项目。他发现，项目中在数学上最有趣的部分，形式化起来比较容易，而技术上看起来最显