借助 Lean，陶哲轩又开端了新的项目。
「由 Alex Kontorovich 和我领导的一个新的 Lean 形式化项目刚刚正式宣布，该项目旨在形式化素数定理（prime number theorem，PNT）的证明，以及随同而来的复分析和解析数论的支撑机制，并方案给出进一步的结果如 Chebotarev 密度定理。」著名数学家陶哲轩在个人博客中写道。
素数定理是数学中的一个重要定理，描绘了素数在自然数中的散布规律，该定理在数论中是一个比较重要的研讨方向。
形式化证明本质上是一种计算机程序，但与 C++ 或 Python 中的传统程序不同，证明的正确性能够用证明助手（比如 Lean 言语）来验证。举例来说，陶哲轩在论文《A MACLAURIN TYPE INEOUALITY》中给出的证明只有不到一页，但形式化证明使用了 200 行 Lean 言语。
而陶哲轩的协作者 Alex Kontorovich 也是一位非常著名的数学家，现为罗格斯大学数学系特聘教授，主要研讨方向是数论。
目前，这两位数学家协作的 Lean 形式化项目「PrimeNumberTheoremAnd」已经上传到 GitHub 上。
由于该项目刚树立不久，陶哲轩以及 Alex Kontorovich 还为此构建了一幅蓝图：
蓝图地址：alexkontorovich.github.io/PrimeNumber…
能够看出该蓝图包括 5 个部分：
榜首部分介绍了项目的首要方针是在 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 已成为数学研讨中的得力助手。