search
HomeTechnology peripheralsAITao 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.

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

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 Zhexuans new project: proving the prime number theorem in Lean, the research blueprint is ready

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.

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

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

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

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:

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

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!

Statement
This article is reproduced at:机器之心. If there is any infringement, please contact admin@php.cn delete
You Must Build Workplace AI Behind A Veil Of IgnoranceYou Must Build Workplace AI Behind A Veil Of IgnoranceApr 29, 2025 am 11:15 AM

In John Rawls' seminal 1971 book The Theory of Justice, he proposed a thought experiment that we should take as the core of today's AI design and use decision-making: the veil of ignorance. This philosophy provides a simple tool for understanding equity and also provides a blueprint for leaders to use this understanding to design and implement AI equitably. Imagine that you are making rules for a new society. But there is a premise: you don’t know in advance what role you will play in this society. You may end up being rich or poor, healthy or disabled, belonging to a majority or marginal minority. Operating under this "veil of ignorance" prevents rule makers from making decisions that benefit themselves. On the contrary, people will be more motivated to formulate public

Decisions, Decisions… Next Steps For Practical Applied AIDecisions, Decisions… Next Steps For Practical Applied AIApr 29, 2025 am 11:14 AM

Numerous companies specialize in robotic process automation (RPA), offering bots to automate repetitive tasks—UiPath, Automation Anywhere, Blue Prism, and others. Meanwhile, process mining, orchestration, and intelligent document processing speciali

The Agents Are Coming – More On What We Will Do Next To AI PartnersThe Agents Are Coming – More On What We Will Do Next To AI PartnersApr 29, 2025 am 11:13 AM

The future of AI is moving beyond simple word prediction and conversational simulation; AI agents are emerging, capable of independent action and task completion. This shift is already evident in tools like Anthropic's Claude. AI Agents: Research a

Why Empathy Is More Important Than Control For Leaders In An AI-Driven FutureWhy Empathy Is More Important Than Control For Leaders In An AI-Driven FutureApr 29, 2025 am 11:12 AM

Rapid technological advancements necessitate a forward-looking perspective on the future of work. What happens when AI transcends mere productivity enhancement and begins shaping our societal structures? Topher McDougal's upcoming book, Gaia Wakes:

AI For Product Classification: Can Machines Master Tax Law?AI For Product Classification: Can Machines Master Tax Law?Apr 29, 2025 am 11:11 AM

Product classification, often involving complex codes like "HS 8471.30" from systems such as the Harmonized System (HS), is crucial for international trade and domestic sales. These codes ensure correct tax application, impacting every inv

Could Data Center Demand Spark A Climate Tech Rebound?Could Data Center Demand Spark A Climate Tech Rebound?Apr 29, 2025 am 11:10 AM

The future of energy consumption in data centers and climate technology investment This article explores the surge in energy consumption in AI-driven data centers and its impact on climate change, and analyzes innovative solutions and policy recommendations to address this challenge. Challenges of energy demand: Large and ultra-large-scale data centers consume huge power, comparable to the sum of hundreds of thousands of ordinary North American families, and emerging AI ultra-large-scale centers consume dozens of times more power than this. In the first eight months of 2024, Microsoft, Meta, Google and Amazon have invested approximately US$125 billion in the construction and operation of AI data centers (JP Morgan, 2024) (Table 1). Growing energy demand is both a challenge and an opportunity. According to Canary Media, the looming electricity

AI And Hollywood's Next Golden AgeAI And Hollywood's Next Golden AgeApr 29, 2025 am 11:09 AM

Generative AI is revolutionizing film and television production. Luma's Ray 2 model, as well as Runway's Gen-4, OpenAI's Sora, Google's Veo and other new models, are improving the quality of generated videos at an unprecedented speed. These models can easily create complex special effects and realistic scenes, even short video clips and camera-perceived motion effects have been achieved. While the manipulation and consistency of these tools still need to be improved, the speed of progress is amazing. Generative video is becoming an independent medium. Some models are good at animation production, while others are good at live-action images. It is worth noting that Adobe's Firefly and Moonvalley's Ma

Is ChatGPT Slowly Becoming AI's Biggest Yes-Man?Is ChatGPT Slowly Becoming AI's Biggest Yes-Man?Apr 29, 2025 am 11:08 AM

ChatGPT user experience declines: is it a model degradation or user expectations? Recently, a large number of ChatGPT paid users have complained about their performance degradation, which has attracted widespread attention. Users reported slower responses to models, shorter answers, lack of help, and even more hallucinations. Some users expressed dissatisfaction on social media, pointing out that ChatGPT has become “too flattering” and tends to verify user views rather than provide critical feedback. This not only affects the user experience, but also brings actual losses to corporate customers, such as reduced productivity and waste of computing resources. Evidence of performance degradation Many users have reported significant degradation in ChatGPT performance, especially in older models such as GPT-4 (which will soon be discontinued from service at the end of this month). this

See all articles

Hot AI Tools

Undresser.AI Undress

Undresser.AI Undress

AI-powered app for creating realistic nude photos

AI Clothes Remover

AI Clothes Remover

Online AI tool for removing clothes from photos.

Undress AI Tool

Undress AI Tool

Undress images for free

Clothoff.io

Clothoff.io

AI clothes remover

Video Face Swap

Video Face Swap

Swap faces in any video effortlessly with our completely free AI face swap tool!

Hot Tools

Atom editor mac version download

Atom editor mac version download

The most popular open source editor

VSCode Windows 64-bit Download

VSCode Windows 64-bit Download

A free and powerful IDE editor launched by Microsoft

Zend Studio 13.0.1

Zend Studio 13.0.1

Powerful PHP integrated development environment

SublimeText3 English version

SublimeText3 English version

Recommended: Win version, supports code prompts!

Notepad++7.3.1

Notepad++7.3.1

Easy-to-use and free code editor