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

AIGC动态欢迎阅读

原标题：AI颠覆数学研究！陶哲轩借AI数学猜想，形式化成功惊呆数学圈

关键字：报告,目标,数学,气泡,人类

文章来源：新智元

内容字数：8260字

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

原文链接：点此阅读原文：AI颠覆数学研究！陶哲轩借AI数学猜想，形式化成功惊呆数学圈

联系作者

文章来源：新智元

作者微信：AI_era

作者简介：智能+中国主平台，致力于推动中国从互联网+迈向智能+新纪元。重点关注人工智能、机器人等前沿领域发展，关注人机融合、人工智能和机器人对人类社会与文明进化的影响，领航中国新智能时代。