Tao Zhexuan's new project: proving the prime number theorem in Lean, the research blueprint is ready

With the help of Lean, Tao Zhexuan started a new project.

"A new Lean formalization project led by Alex Kontorovich and myself has just been officially announced, which aims to formalize the prime number theorem (prime number theorem (PNT), as well as the accompanying support mechanisms of complex analysis and analytic number theory, and plans to give further results such as Chebotarev’s density theorem.” Famous mathematician Terence Tao wrote on his personal blog.

The prime number theorem is an important theorem in mathematics, which describes the distribution of prime numbers in natural numbers. This theorem is an important research direction in number theory.

Formal proof is essentially a computer program, but unlike traditional programs in C or Python, the correctness of the proof can be verified using a proof assistant (such as Lean language) to verify. For example, the proof given by Terence Tao in his paper "A MACLAURIN TYPE INEOUALITY" is less than one page, but the formal proof uses 200 lines of Lean language.

Tao Zhexuan’s collaborator Alex Kontorovich is also a very famous mathematician and is currently a distinguished professor in the Department of Mathematics at Rutgers University. His main research direction is number theory.

Currently, the Lean formal project "PrimeNumberTheoremAnd" collaborated by these two mathematicians has been uploaded to GitHub.

Project address: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd

Because the project has just been established. , Terence Tao and Alex Kontorovich also constructed a blueprint for this:

Blueprint address: https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/

It can be seen that the blueprint contains 5 parts:

The first part introduces the primary goal of the project is to prove prime numbers in Lean theorem. They say the problem remains one of the outstanding ones on Wiedijk's list of 100 theorems requiring formalization. It is worth noting that PNT has been formalized previously, in Isabelle by Avigad et al. And the goal of this project is to extend this work to prime numbers in series (Dirichlet's theorem), Chebotarev's density theorem, and more.

Currently, the following three methods can be considered to achieve the above goals:

The fastest is proposed by Michael Stoll "Eulerian Product" project, the project's proof of PNT only lacks the Wiener-Ikehara Tauberian theorem (corresponding to the second part).

The second is to develop some complex analysis, including residue calculus on rectangles, argument principle and Mellin transformation, leading to a prime number theorem (PNT) containing only asymptotic formulas ) (corresponding to the third part).

The third method is also the most common of the three methods, including Hadamard factor decomposition theorem, Hoffstein-Lockhart and other processes (corresponding to the fourth part).

The last part is the basic inference.

In fact, looking back at Tao Zhexuan’s previous research, he mentioned Lean many times. Simply put, Lean is a programming language that helps mathematicians verify theorems, where users can write and verify proofs. Compared with the original Lean, the latest Lean 4 version has many optimizations, including a faster compiler, improved error handling, and better integration with external tools. Now, Terence Tao and others have used this tool for the formal proof of the prime number theorem. It can be seen that Lean has become a powerful assistant in mathematical research.

The above is the detailed content of Tao Zhexuan's new project: proving the prime number theorem in Lean, the research blueprint is ready. For more information, please follow other related articles on the PHP Chinese website!