加州理工华人用AI颠覆数学证明！提速5倍震惊陶哲轩，80%数学步骤全自动化

AIGC动态欢迎阅读

原标题：加州理工华人用AI颠覆数学证明！提速5倍震惊陶哲轩，80%数学步骤全自动化
关键字：策略,定理,前提,目标,报告
文章来源：新智元
内容字数：13184字

内容摘要：

新智元报道编辑：编辑部
【新智元导读】让陶哲轩大神赞不绝口的形式化研究神器Lean，运行LLM的推理却有个bug。最近，加州理工团队解决了这个bug，把80%以上的数学证明步骤，都自动化了！Lean Copilot，让陶哲轩等众多数学家赞不绝口的这个形式化数学工具，又有超强进化了？
就在刚刚，加州理工教授Anima Anandkumar宣布，团队发布了Lean Copilot论文的扩展版本，并且更新了代码库。
论文地址：https://arxiv.org/pdf/2404.12534.pdf
最新实验表明，这个Copilot工具，可以自动化80%以上的数学证明步骤了！这个纪录，比以前的基线aesop还要好2.3倍。
并且，和以前一样，它在MIT许可下是开源的。
而对此做出巨大贡献的，是一位华人小哥宋沛洋，他是UCSB的荣誉CS本科生，加州理工学院计算+数学科学（CMS）系的SURF研究员。
网友惊呼：所以，陶哲轩现在的数学研究可以原地加速5倍了？
LLM提出证明策略，人类无缝干预团队就发布了这个Lean Copilot的工具，希望启动人类和LLM的协作，编写出100%准确的形式化数学

原文链接：加州理工华人用AI颠覆数学证明！提速5倍震惊陶哲轩，80%数学步骤全自动化

联系作者

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