陶哲轩

陶哲轩上新项目：Lean中证明素数定理，研究蓝图都建好了

借助 Lean，陶哲轩又开始了新的项目。「由 Alex Kontorovich 和我领导的一个新的 Lean 形式化项目刚刚正式宣布，该项目旨在形式化素数定理（prime number theorem，PNT）的证明，以及伴随而来的复分析和解析数论的支持机制，并计划给出进一步的结果如 Chebotarev 密度定理。」著名数学家陶哲轩在个人博客中写道。素数定理是数学中的一个重要定理，描述了素数在自然数中的分布规律，该定理在数论中是一个比较重要的研究方向。形式化证明本质上是一种计算机程序，但与 C 或 Pytho

1/31/2024 3:05:00 PM

机器之心

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

现在，数学辅助证明工具都用上了大模型。「我预计，如果使用得当，到 2026 年，AI 将成为数学研究和许多其他领域值得信赖的合著者。」数学家陶哲轩在之前的一篇博客中说道。陶哲轩这样说了，也这样做了。他最近一直在用 GPT-4、Copilot、Lean 等工具进行数学研究，并且还在 AI 的帮助下发现了自己论文中的一处隐藏 bug。不仅如此，前几天，陶哲轩表示：对多项式 Freiman-Ruzsa 猜想（PFR）的证明进行形式化的 Lean4 项目成功完成，并且耗时仅三周时间。Lean 编译器也报告该猜想符合标准公理

12/18/2023 3:08:00 PM

机器之心

陶哲轩用 AI 形式化的证明究竟是什么？一文看懂 PFR 猜想的前世今生

正是包括两位菲尔兹奖获得者在内四位数学家的坚持，才得以证明了一个堪称「加性组合学圣杯」的猜想，其中 AI 辅助证明起到了不可磨灭的作用。12 月 5 日，著名数学家、菲尔兹奖获得者陶哲轩在社交网络宣布：对多项式 Freiman-Ruzsa 猜想（PFR）的证明进行形式化的 Lean4 项目成功完成，并且耗时仅三周时间，其依赖图的全部节点都带上了「可爱的绿色阴影」。Lean 编译器也报告该猜想符合标准公理，可以说这是计算机和 AI 辅助证明的一项巨大成功。但多项式 Freiman-Ruzsa 猜想究竟是什么？为什么对

12/11/2023 3:38:00 PM

机器之心

陶哲轩上手Copilot：不可思议，它能从定理名字猜出我想要的方向

尝鲜 GPT-4 之后，陶哲轩又用上了 Github Copilot。这一次，他的试用场景是学习 Lean 语言并利用其形式化数学定理。对于大模型来说，形式化的定理证明也算一种挑战。形式化证明本质上是一种计算机程序，但与 C 或 Python 中的传统程序不同，证明的正确性可以用证明助手（比如 Lean 语言）来验证。定理证明是代码生成的一种特殊形式，在评估上非常严格，没有让模型产生幻觉的空间。而陶哲轩提到的定理，来自 10 月 9 日的一篇论文：论文中的这个证明只有不到一页，但陶哲轩的形式化证明使用了 200

10/23/2023 3:49:00 PM

机器之心