AI Proves First Fields Medal Result, Blazes Through 200,000 Lines of Code in Two Weeks, Stirring Up the Math Community

In 2026, the field of mathematics is in a dire situation! A proof that top scholars failed to advance has been completed, and even a Fields Medalist has been pointed out for logical flaws in their paper. When AI intelligent agents can independently take over the verification of truth, how long can the existing scientific research paradigm last?

It's outrageous! The field of mathematics has been raided by AI Gauss.

In just 5 days, it finished a hard task that humans couldn't handle in 15 months.

Viazovska's 8 - dimensional and 24 - dimensional sphere packing proofs were converted into 200,000 lines of Lean code, with 90 times the efficiency!

Human elites VS AI? It's like comparing an abacus to a quantum computer. Humans don't stand a chance.

Netizens complained: Help! This AI is extremely competitive. Does even DeepMind have to admit defeat?

Gauss Sends "Error - Correction Email" to Fields Medalist

The 8 - dimensional and 24 - dimensional proofs target the sphere packing problem.

In n - dimensional Euclidean space, how to arrange spheres of the same size (without overlap) as densely as possible and prove that a specific lattice achieves the optimal arrangement.

This problem has a history of hundreds of years. It's difficult to strictly prove the optimality in most dimensions, but the 8 - dimensional and 24 - dimensional cases are special.

In 2022, Viazovska won the Fields Medal with her 8 - dimensional E8 and 24 - dimensional Leech lattice sphere packing proofs, becoming the second female Fields Medalist.

Paper link: http://arxiv.org/abs/1603.04246

Paper link: https://arxiv.org/abs/1603.06518

But now, AI is making inroads!

Viazovska's paper has dozens of pages, with human logic compressed into natural language.

But in the eyes of a computer, words like "it should be so" are incomprehensible.

Before Gauss intervened, a team spent 15 months trying to formalize this Fields Medal - winning result in Lean.

Limited by the bandwidth of human cognition and the decline of attention, the project advanced slowly.

From 15 months to 5 days, the computing power of humans in handling ultra - large - scale logical chains has reached its limit.

8 - Dimensional Proof Formalization: AI Exposes Flaws in Fields Medal Paper

At its core, Gauss is a closed - loop reasoning agent that outperforms old - fashioned code. Its retrieval module scans thousands of literatures to supplement background knowledge, and its reconstruction module directly converts to Lean code and performs real - time compilation and verification.

When processing the 8 - dimensional E8 modular coefficients of Viazovska's work, Gauss found 30 logical flaws.

In the Lean community, these steps that have not been verified by machines are usually marked as "sorry".

For human developers, filling these "sorry" gaps means consulting a vast amount of literature and translating it into machine - recognizable syntax.

The turning point occurred in an inequality derivation on page 14 of the paper.

After 4096 consecutive reasoning steps, Gauss reported a compilation error and pointed out a typesetting and micro - logical flaw in the original paper.

Without human intervention, Gauss autonomously searched the historical theorem library, reconstructed the boundary conditions of this step, and completed the missing proof.

Previously, human mathematicians were always in charge of logic, and AI was only responsible for execution. Now, Gauss has shown a more sensitive error - correction intuition than humans.

For the academic community, the complete formalization of the 8 - dimensional proof is a watershed.

It not only produced tens of thousands of lines of high - quality Lean code but also proved that reasoning agents can identify and repair human logical blind spots.

This ability pushes mathematical verification from the fuzzy area to the absolute digital value of 100% operability.

24 - Dimensional Proof: Autonomous Reconstruction without a Blueprint

In the field of mathematics, the 24 - dimensional Leech Lattice is far more complex than the 8 - dimensional E8 lattice.

This time, Gauss has no pre - set blueprint to refer to, and the complexity is significantly higher than the 8 - dimensional case.

In the formalization process of the 8 - dimensional proof, the human team had already built a framework in the Lean community and marked a large number of "sorry" as guides.

But in the 24 - dimensional proof, Gauss faces a logical vacuum.

The difficulty of the 24 - dimensional sphere packing proof lies in its deep coupling with the complex group - theory proof of the uniqueness of the Leech lattice.

The core breakthrough shown by Gauss is reasoning without a blueprint.

When proving that the Leech lattice is the only structure that can achieve the maximum density in 24 - dimensional space, Gauss demonstrated a strong ability to synthesize literature.

Paper link: https://arxiv.org/abs/2601.04567

The system used its retrieval module to locate dozens of relevant papers spanning 30 years.

It understood the main logical line of Viazovska's original paper and, through cross - literature comparison, independently identified external lemmas to be introduced, such as the symmetry characteristics of the Co0 Conway group.

In the in - depth advancement of the 24 - dimensional proof, Gauss needs to generate and verify more than 120,000 lines of Lean code.

At this scale, any logical drift caused by a misunderstanding of the context will lead to an exponential number of error crashes.

Gauss monitors the reasoning chain and calculates the confidence of each inference step in real - time. When the confidence is below the threshold, it triggers a backtracking mechanism and re - searches the mathematical axiom library.

In the 2048th logical block of the 24 - dimensional proof, Gauss independently completed the spectral gap estimation of the Laplacian operator on a specific manifold.

This step was regarded as an "obvious" conclusion in the original paper, but in formal verification, it requires nearly 10,000 lines of proof code.

Gauss completed this logical filling in just 14 hours. The reshaping of high - difficulty intellectual activities by AI has become an autonomous takeover of the entire scientific research chain.

In the arena of logical verification, humans are no longer indispensable.

Paradigm Shift: The Engineering Era of Mathematical Proof

For a long time, the medium for spreading mathematical proofs has been natural - language papers. Although this form is flexible, it comes with a high threshold for understanding and a high cost for logical verification.

The emergence of Gauss marks that mathematics is shifting from natural - language literature to runnable software engineering.

Jesse Han, the CEO of Math, Inc., compares this transformation to the transition of computer science from the punch - card era to the high - level language era.

In the punch - card era, programmers had to pay attention to every underlying physical bit. In the high - level language era, developers can conceive complex system logic at an abstract level.

Jesse Han believes:

The ultimate result of this technology will be to liberate mathematicians... and let them dream of new mathematical worlds.

In the future, mathematicians will turn to higher - level architectural design, and tasks such as mathematical proofs will be automatically completed by reasoning agents like Gauss.

As the underlying language of all natural sciences, the acceleration of the engineering progress of mathematics will directly affect strong - logic fields such as cryptography, quantum computing, and aerospace orbit calculation.

Under this new paradigm, humans will act as conductors, and the onerous deductive reasoning will be handed over to intelligent agents with ASI potential.

Maryna Viazovska was once regarded as the peak of human intelligence. Now, her work has been transformed into 202,000 lines of bits in the server.

In this era where truth no longer requires human intermediaries, do we have the courage to follow the path opened by AI and touch the unknown territories beyond human intuition?

References

https://spectrum.ieee.org/ai-proof-verification?share_id=9202657&utm_campaign=RebelMouse&utm_content=IEEE+Spectrum&utm_medium=social&utm_source=twitter

https://x.com/mathematics_inc/status/2028542388717986135?s=20

This article is from the WeChat official account "New Intelligence Yuan". Author: Qing Qing. Republished by 36Kr with permission.