清华校友用AI162个高数定理，智能体LeanAgent攻克困扰陶哲轩难题！

AIGC动态欢迎阅读

原标题：清华校友用AI162个高数定理，智能体LeanAgent攻克困扰陶哲轩难题！
关键字：定理,代码,可塑性,数据,数学
文章来源：新智元
内容字数：0字

内容摘要：

新智元报道编辑：编辑部 HYZ
【新智元导读】就在刚刚，清华校友用AI证明了162个未被人类证明的数学定理，解决了AI无法解决陶哲轩对多项式Freiman-Ruzsa猜想的形式化难题！诺贝尔物理学奖和化学奖被AI「包圆」后，人们再次确信：基础科学研究的范式，已经被AI从根本上改变。
果然，就在刚刚，AI成功证明了162个以前未被证明的数学定理，再次印证了这一点。
到目前为止，LLM仍然是静态的，无法在线学习新知识，更别提证明高数定理了。
对此，来自加州理工、斯坦福和威大的研究人员提出了LeanAgent——一个终身学习，并能证明定理的AI智能体。
论文地址：https://arxiv.org/abs/2410.06209
LeanAgent会根据数学难度优化的学习轨迹课程，来提高学习策略。并且，它还有一个动态数据库，有效管理不断扩展的数学知识。
值得一提的是，整个学习过程中，它既能自我学习新知识，同时不会遗忘已具备的能力。
实验结果发现，LeanAgent从来自23个不同Lean代码库中，成功证明162个此前未被人类证明的数学定理。
相较于基于Lean数据微调大模型，LeanAgen

原文链接：清华校友用AI162个高数定理，智能体LeanAgent攻克困扰陶哲轩难题！

联系作者

文章来源：新智元
作者微信：
作者简介：