Shing-Tung Yau's student has made another remarkable contribution, marking the world's first successful formal verification of the proof of the generalized Poincaré conjecture.

Just now, another major piece of news has emerged in the mathematics community.

In September, the successful formal verification of the "Poincaré Conjecture" by AI has already shocked the mathematics world.

Just now, a top academic team led by Ayush Khaitan, in collaboration with the NVIDIA Humanfia Team, has successfully completed the full Lean formalization of the Thurston Geometrization Conjecture!

The "Century Proof" by Hamilton and Perelman spans hundreds of pages, and even top human scholars need several years to go through it thoroughly.

Following the famous Poincaré Conjecture proven in September this year, this achievement has finally been transformed into lines of code with the assistance of AI.

4.7 million lines of code were completed in only about two weeks.

This is another monument in the history of mathematics, and a sign that AI-assisted high-order geometric analysis has entered an "era of explosive development".

AI-assisted formal mathematics has officially broken into the "no man's land" of the most profound high-order geometric analysis of humanity.

Amazing! The Poincaré Conjecture has been extended to the complete Geometrization Conjecture

If someone tells you that a team wrote 4.7 million lines of error-free modern mathematics code in two weeks, you must think they are crazy.

But this is exactly what just happened in reality.

Recently, Jared Duker Lichtman, Assistant Professor of Mathematics at Stanford University, exclaimed:

Truly an astonishing piece of work.

The proof of the Poincaré Conjecture has been extended to the full Geometrization Conjecture, and all of this is completed in Lean!

The result was published by Ayush Khaitan, a mathematics and AI scholar at Princeton University. In his tweet, he introduced this extremely strong cross-disciplinary lineup.

Take a look at this hardcore team list:

Bennett Chow: Student of Shing-Tung Yau, Professor of the Department of Mathematics at the University of California, San Diego, and an absolute authority and leading figure in the field of Ricci flow.

Ziyang Qin and Yuan Liao: The absolute leaders of the formalization work of the project.

Ayush Khaitan: Scholar at Princeton University, the core driving force of the project.

NVIDIA Humanfia Team (Jui-Hui Chung & Ligeng Zhu): Representing the cutting-edge force of NVIDIA, the world's top AI computing power giant.

With the collaboration of this super team, a miracle was born.

Ayush revealed that this proof has approximately 4.7 million lines of code.

Based on the previous work of about 2 million lines of code completed by Chow, Liao and Qin, the additional 2.7 million lines of code were written in just about two weeks!

At present, this great project has been fully open-sourced on GitHub.

https://github.com/qinz1yang/differential-geometry

Dimensionality Reduction Strike: From "Poincaré Conjecture" to "Full Geometrization Conjecture", What Exactly Did They Prove?

Why are Stanford mathematicians so excited?

First of all, we need to understand how difficult the Thurston Geometrization Conjecture actually is.

Everyone has heard of the "Poincaré Conjecture".

It discusses the following question: If every closed curve in a three-dimensional space can be contracted to a point, is this space necessarily equivalent to a three-dimensional sphere?

From 2002 to 2003, the Russian mathematical genius Grigori Perelman emerged out of nowhere, proved the Poincaré Conjecture with three preprint papers, and then refused to accept the million-dollar prize, keeping his remarkable achievement low-key.

But the Poincaré Conjecture is actually just the "tip of the iceberg" of a grand blueprint. This blueprint is called the "Thurston Geometrization Conjecture".

In other words, the Poincaré Conjecture teaches you how to recognize a "spherical object", while the Thurston Geometrization Conjecture draws a full "periodic table of elements" for the entire three-dimensional universe.

It points out that any three-dimensional manifold can eventually be accurately cut into several pieces. More importantly, each piece must belong to one of 8 standard geometric structures!

Back then, Perelman proved the Thurston Geometrization Conjecture, and incidentally proved the Poincaré Conjecture at the same time.

The unique trick he used is called "Ricci Flow and Surgery Theory".

This is like using a "geometric iron" (the Ricci flow equation) to smooth out the distorted space. When encountering a stubborn knot (singularity) that cannot be smoothed out, perform a "surgical operation" to cut it off, seal it up, and then continue ironing.

This theory is extremely profound, and even dozens of the top mathematicians in the world spent two or three years to fully verify Perelman's proof.

And today, these great scholars and engineers have completely implanted this theory at the peak of human intelligence into the mind of the computer!

The complete Lean proof of the Thurston Geometrization Conjecture means that machines already have the ability to handle advanced differential geometry, topology and partial differential equations.

Machines have officially broken into the "no man's land" of high-order geometry.

Unpack the GitHub code repository: What exactly is written in these 4.7 million lines of code?

If you open this GitHub repository named differential-geometry, you will feel a strong "hardcore shock".

Link: https://github.com/qinz1yang/differential-geometry

This is a "digital Great Wall of modern differential geometry" built with machine language.

In Lean, this interactive theorem prover, the computer does not know what "it is obvious to deduce" means, it only recognizes the underlying logical axioms. In order to make the machine understand the Thurston Geometrization Conjecture, the team must define the rules of the entire universe in the code from scratch.

Judging from the technical details of the repository, the team has hardcore filled a large number of missing basic infrastructures in Lean's official mathematical library (Mathlib).

They reconstructed Riemannian geometry from the bottom layer.

The code defines extremely complex Manifolds, Tangent Bundles, Tensor Fields and Riemannian Metrics.

The team used rigorous generic programming to finally make the machine "recognize" what a curved space is.

In traditional mathematical papers, Ricci flow is nothing more than a partial differential equation

.

But in the GitHub repository, the team needs tens of thousands of lines of code to precisely define "time-dependent metric evolution", "local calculation of Ricci curvature tensor" and the extremely complex existence boundary of partial differential equation solutions.

The most difficult part of Perelman's proof is undoubtedly "Surgery Theory".

How to realize the "cutting" and "suturing" of an abstract space in the code?

The team introduced complex topological connectivity and geometric decomposition algorithms in the code base, transforming geometric singularity processing into a logical tree that the computer can run and verify step by step.

Crazy output in two weeks: NVIDIA joined in, large models take over the "code production line"

The most exciting set of data is: two weeks, nearly 2.7 million lines of new code, 4.7 million lines in total.

In the software engineering industry, a 2.7 million-line project is enough for a senior development team of dozens of people to work overtime continuously for a whole year.

In the Lean language, which has extremely high logical density and each line of code requires a very long compilation verification time, it is absolutely impossible to complete writing it in two weeks purely by manpower!

How did they do it?

The answer is obvious: the NVIDIA Humanfia team brought the "dimensionality reduction strike" of large models and automated reasoning.

NVIDIA not only provides the strongest computing power on the earth, but they are also exploring how to make AI directly assist the most cutting-edge basic scientific research.

Although the official has not yet disclosed all the details of AI generation, the "industrialized" proof assembly line can be inferred from the code volume that increased sharply in a short period of time.

Top mathematicians such as Chow, Liao and Qin are responsible for drawing the "tactical map", breaking down the huge Geometrization Conjecture into thousands of lemmas and sub-goals.

The NVIDIA team uses LLM and automated scripts to generate a huge amount of underlying proof code, complete tedious algebraic deductions and exhaustive enumeration of boundary conditions frantically based on the context provided by humans.

Finally, all codes are sent to the Lean compiler for ruthless "logical quality inspection". If they fail, they will be sent back to rewrite until the green light turns on.

This is not only a major event in the mathematics community, but also an absolute focus in the history of AI evolution!

Current large language models still have "hallucinations" in complex long-chain logical reasoning, and the ultimate weapon to solve the logical defects of large models is mathematical formalization.

If AI can skillfully generate Lean code to prove products at the peak of human intelligence such as the Thurston Geometrization Conjecture, then it is really only one step away from AI "proposing new conjectures and giving proofs on its own".

Laying highways for the mathematical universe, a new era has already begun

The complete formalization of the Thurston Geometrization Conjecture is far more than just completing a high-difficulty "code translation". What it leaves to the world is a valuable digital asset.

Through the differential-geometry project on GitHub, the team has left a set of differential geometry code library that has undergone "absolute truth verification" for all mankind.

This means that in the future, when mathematicians all over the world want to study multidimensional manifolds, the geometric structure of black holes and even the evolution of space-time in the computer, they can directly call the library they wrote!

This is a great project where predecessors plant trees and descendants enjoy the shade.

From Poincaré writing down that famous conjecture more than a hundred years ago, to Thurston depicting the grand blueprint of the three-dimensional universe.

From Perelman doing calculations in his apartment in St. Petersburg, to today when scholars such as Ayush Khaitan, Ziyang Qin, Yuan Liao, Bennett Chow, together with NVIDIA, use 4.7 million lines of code to make the machine completely "enlightened"...

The human pursuit of truth is like a relay race.

AI did not take away mathematicians' jobs, but gave them a set of "starships" to explore the universe.

The pace of human beings solving difficult problems will erupt with an unprecedented acceleration.

References:

https://x.com/ayushkhaitan343/status/2108654050203840528?s=20

This article is from the WeChat official account "Xinzhiyuan", Author: David Aeneas, 36Kr is authorized to republish it.