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

AIGC动态欢迎阅读

原标题：陶哲轩上新项目：Lean中证明素数定理，研究蓝图都建好了
关键字：定理,素数,数学家,数论,项目
文章来源：机器之心
内容字数：2731字

内容摘要：

机器之心报道
编辑：陈萍借助 Lean，陶哲轩又开始了新的项目。「由 Alex Kontorovich 和我领导的一个新的 Lean 形式化项目刚刚正式宣布，该项目旨在形式化素数定理（prime number theorem，PNT）的证明，以及伴随而来的复分析和解析数论的支持机制，并计划给出进一步的结果如 Chebotarev 密度定理。」著名数学家陶哲轩在个人博客中写道。素数定理是数学中的一个重要定理，描述了素数在自然数中的分布规律，该定理在数论中是一个比较重要的研究方向。
形式化证明本质上是一种计算机程序，但与 C++ 或 Python 中的传统程序不同，证明的正确性可以用证明助手（比如 Lean 语言）来验证。举例来说，陶哲轩在论文《A MACLAURIN TYPE INEOUALITY》中给出的证明只有不到一页，但形式化证明使用了 200 行 Lean 语言。而陶哲轩的合作者 Alex Kontorovich 也是一位非常著名的数学家，现为罗格斯大学数学系特聘教授，主要研究方向是数论。目前，这两位数学家合作的 Lean 形式化项目「PrimeNumberTheoremAnd」

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