![](https://cdn.jiqizhixin.com/assets/code-modal__close-c158a550a9982aa92801c046548d72945aa912de6f2a012513132fdc02dfc379.png)
Auto Byte
专注未来出行及智能汽车科技
![](https://cdn.jiqizhixin.com/assets/auto-byte__qr-code-89b58c6d2398c12b7def0f2538cac5ff08727062918f9bad97f25b1d61aac000.png)
微信扫一扫获取更多资讯
![](https://cdn.jiqizhixin.com/assets/code-modal__close-c158a550a9982aa92801c046548d72945aa912de6f2a012513132fdc02dfc379.png)
Science AI
关注人工智能与其他前沿技术、基础学科的交叉研究与融合发展
![](https://cdn.jiqizhixin.com/assets/science-ai__qr-code-a12e4635c8d3968645bd2b6371981b65b0d21058c5a2c216aef80015b4eb7e43.png)
微信扫一扫获取更多资讯
陶哲轩上新项目:Lean中证明素数定理,研究蓝图都建好了
「由 Alex Kontorovich 和我领导的一个新的 Lean 形式化项目刚刚正式宣布,该项目旨在形式化素数定理(prime number theorem,PNT)的证明,以及伴随而来的复分析和解析数论的支持机制,并计划给出进一步的结果如 Chebotarev 密度定理。」著名数学家陶哲轩在个人博客中写道。![图片](https://image.jiqizhixin.com/uploads/editor/1e4fdcf2-7017-441f-aaa5-c12086220e31/640.png)
素数定理是数学中的一个重要定理,描述了素数在自然数中的分布规律,该定理在数论中是一个比较重要的研究方向。形式化证明本质上是一种计算机程序,但与 C++ 或 Python 中的传统程序不同,证明的正确性可以用证明助手(比如 Lean 语言)来验证。举例来说,陶哲轩在论文《A MACLAURIN TYPE INEOUALITY》中给出的证明只有不到一页,但形式化证明使用了 200 行 Lean 语言。![图片](https://image.jiqizhixin.com/uploads/editor/8df8a147-5329-41c1-b011-1191cb6df27b/640.png)
而陶哲轩的合作者 Alex Kontorovich 也是一位非常著名的数学家,现为罗格斯大学数学系特聘教授,主要研究方向是数论。![图片](https://image.jiqizhixin.com/uploads/editor/775e1de8-760d-495a-9f9e-cc679c158388/640.png)
目前,这两位数学家合作的 Lean 形式化项目「PrimeNumberTheoremAnd」已经上传到 GitHub 上。![图片](https://image.jiqizhixin.com/uploads/editor/46249b24-f152-4eb6-9a08-88345bd7c748/640.png)
项目地址:https://github.com/AlexKontorovich/PrimeNumberTheoremAnd因为该项目刚建立不久,陶哲轩以及 Alex Kontorovich 还为此构建了一幅蓝图:![图片](https://image.jiqizhixin.com/uploads/editor/9edc037f-9a04-419f-af2f-3a41c320d41e/640.png)
蓝图地址:https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/第一部分介绍了项目的首要目标是在 Lean 中证明素数定理。他们表示该问题仍然是 Wiedijk 列出的需要形式化的 100 个定理中突出的问题之一。值得注意的是,PNT 之前已被形式化过,由 Avigad 等人在 Isabelle 中完成。而该项目的目标是将这项工作扩展到级数中的素数(Dirichlet 定理)、Chebotarev 密度定理等等。最快的是 Michael Stoll 提出的「欧拉积」项目,该项目对 PNT 的证明只缺少 Wiener-Ikehara Tauberian 定理(对应第二部分)。第二种是开发一些复分析,包括 residue calculus on rectangles 、 argument principle 和 Mellin 变换,从而得出一个仅包含渐近公式的素数定理(PNT)的证明(对应第三部分)。第三种方法,也是三种方法中最通用的一种,包括阿达马因子分解定理、Hoffstein-Lockhart 等过程(对应第四部分)。其实回顾陶哲轩以往的研究,他都多次都提到过 Lean。简单来讲,Lean 是一种可帮助数学家验证定理的编程语言,用户可以在其中编写和验证证明。相比初代 Lean,现在最新的 Lean 4 版本进行了多项优化,包括更快的编译器、改进的错误处理和更好的与外部工具集成的能力等。现在,陶哲轩他们又将该工具用于素数定理的形式化证明,可见 Lean 已成为数学研究中的得力助手。 产业Alex Kontorovich素数定理陶哲轩