陶哲轩青睐的证明助手Lean，用上了大模型

AIGC动态欢迎阅读

原标题：陶哲轩青睐的证明助手Lean，用上了大模型

关键字：报告,数学,模型,策略,定理

文章来源：机器之心

内容字数：4657字

内容摘要：机器之心报道编辑：陈萍现在，数学辅助证明工具都用上了大模型。「我预计，如果使用得当，到 2026 年，AI 将成为数学研究和许多其他领域值得信赖的合著者。」数学家陶哲轩在之前的一篇博客中说道。陶哲轩这样说了，也这样做了。他最近一直在用 GPT-4、Copilot、Lean 等工具进行数学研究，并且还在 AI 的帮助下发现了自己论文中的一处隐藏 bug。不仅如此，前几天，陶哲轩表示：对多项式 Freiman-Ruzsa 猜想（PFR）的证明进行形式化的 Lean4 项目成功完成，并且耗时仅三周时间。Lean 编译器也报告该猜想符合标准公理，可以说这是计算机和 AI 辅助证明的一项巨大成功。关于上述研究的更多内容，感兴趣的读者可以参考《》。看到这，细心的读者可能已经发现了端倪，陶大神在进行数学研究时，多次都提到过 Lean。简单来讲，Lean 是一种可帮助数学家验证定理的编程语言，用户可以在其…

原文链接：点此阅读原文：陶哲轩青睐的证明助手Lean，用上了大模型

联系作者

文章来源：机器之心

作者微信：almosthuman2014

作者简介：专业的人工智能媒体和产业服务平台