Künstliche Intelligenz beweist das erste Ergebnis eines Fields-Medalisten, schreibt 200.000 Codezeilen in zwei Wochen, und die Mathematikwelt ist in Aufruhr.

In 2026, mathematics has fallen into a crisis! A proof that leading scientists were unable to advance was successfully carried out, and even the winner of the Fields Medal has been shown to have logical flaws in his dissertation. How long can the existing scientific research paradigm be maintained if artificial intelligence agents can autonomously take over the verification of truths?

That's incredible! Mathematics is being plundered by the AI Gauss.

Within just 5 days, it has solved a problem that humans couldn't solve in 15 months.

Viazovska's proof for the 8- and 24-dimensional sphere packing was converted into 200,000 lines of Lean code, which represents a 90-fold efficiency compared to humans!

The battle between human elites and AI? That's like the encounter between an abacus and a quantum computer. Humans don't stand a chance.

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

Gauss sends correction emails to the Fields Medalist

The proofs for the 8- and 24-dimensions relate to the sphere packing problem.

In an n-dimensional Euclidean space, it's about how spheres of the same diameter (without overlapping) can be arranged as densely as possible, and to prove that a certain lattice achieves the optimal arrangement.

This problem has a history of several hundred years. In most dimensions, it's difficult to strictly prove the optimal arrangement, but the 8- and 24-dimensions are special cases.

In 2022, Viazovska outperformed everyone else with her proof for the 8-dimensional E8 and 24-dimensional Leech lattice sphere packing and became the second woman to receive the Fields Medal.

Link to the dissertation: http://arxiv.org/abs/1603.04246

Link to the dissertation: https://arxiv.org/abs/1603.06518

But now, the AI has broken through!

Viazovska's dissertation spans several dozen pages, and human logic has been translated into natural language.

But for a computer, a concept like "obviously" is incomprehensible.

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

But due to humans' limited cognitive bandwidth and decreasing attention span, the project progressed slowly.

From 15 months to 5 days - humans' computing power in processing huge logical chains has reached its limit.

Formalization of the 8-dimensional proof: The AI exposes logical errors in the Fields Medal dissertation

The basis of Gauss is a closed loop of inference agents that surpasses the old codes. The search module searches thousands of literature sources to collect background information, and the reconstruction module directly converts the dissertation into Lean code and verifies it in real-time.

When processing Viazovska's 8-dimensional E8 module coefficients, Gauss discovered 30 logical flaws.

In the Lean community, these steps that haven't been verified by the machine are usually marked with "sorry".

For human developers, it means eliminating these "sorry" markings, searching a huge amount of literature, and translating it into machine-readable syntax.

The turning point came in the derivation of an inequality on page 14 of the dissertation.

After 4096 consecutive inference steps, Gauss reported a compilation error and pointed out a typo and a microscopic logical flaw in the original dissertation.

Without human intervention, Gauss autonomously searched the historical theorem database, rebuilt the boundary conditions for this step, and supplemented the missing proof.

Previously, human mathematicians were mainly responsible for logic, and the AI was only responsible for execution. Now, Gauss shows a sharper intuition for error correction than humans.

For science, the complete formalization of the 8-dimensional proof is a milestone.

It has not only produced thousands of lines of high-quality Lean code but also proven that inference agents are able to recognize and correct human logical blind spots.

This ability brings mathematical verification from the gray area into the realm of absolute digital executability.

24-dimensional proof: Autonomous reconstruction without a template

In mathematics, the 24-dimensional Leech lattice is much more complex than the 8-dimensional E8 lattice.

This time, Gauss doesn't have a predefined template, and the complexity is significantly higher than in the 8-dimensional case.

When formalizing the 8-dimensional proof, the human team had already built a framework in the Lean community and set many "sorry" markings as a guide.

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

The problem in proving the 24-dimensional sphere packing lies in its close connection with a complex group theory proof for the uniqueness of the Leech lattice.

The core of Gauss is inference without a template.

In proving that the Leech lattice is the only structure that achieves the maximum density in 24-dimensional space, Gauss has shown a strong ability to synthesize literature.

Link to the dissertation: https://arxiv.org/abs/2601.04567

The system used its search module to find several dozen related dissertations from the past 30 years.

It understood the main logical line of Viazovska's original dissertation and independently recognized, through comparing different literature sources, which external lemmas need to be introduced, such as the symmetry properties of the Conway group Co0.

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

At this scale, any logical drift due to errors in understanding the context can lead to an exponential number of errors.

Gauss monitors the inference chain and calculates the reliability of each inference step in real - time. When the reliability falls below a threshold, it triggers a backtracking mechanism and searches the database of mathematical axioms again.

In the 2048th logical block of the 24-dimensional proof, Gauss independently supplemented the estimation of the spectral gap of the Laplace operator on a certain manifold.

This step was considered "obvious" in the original dissertation, but in formal verification, it requires almost ten thousand lines of proof code.

Gauss supplemented this logical section in just 14 hours. The transformation of highly difficult mental activities by AI has turned into the autonomous takeover of the entire scientific research process.

In the competition of logical verification, humans are no longer irreplaceable.

Paradigm shift: The era of engineering mathematical proofs

For a long time, natural language has been the main communication method for mathematical proofs. Although this form is flexible, the effort for understanding and the cost for logical verification are very high.

The emergence of Gauss marks the transition of mathematics from natural language literature to executable software development.

Jesse Han, the CEO of Math, Inc., compares this change 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 take care of every single physical bit. In the high - level language era, developers can design complex system logics at an abstract level.

Jesse Han says:

The end result of this technology will be the liberation of mathematicians... so that they can invent new mathematical worlds.

In the future, mathematicians will focus on higher - level architectural design, and tasks like mathematical proofs will be automatically done by inference agents like Gauss.

Since mathematics is the foundation of all natural sciences, the acceleration of the engineering process will directly impact areas such as cryptography, quantum computing, and the calculation of spaceflight trajectories.

In this new paradigm, humans will act as conductors, and the laborious deductive inference will be handed over to agents with the potential for strong artificial intelligence.

Maryna Viazovska was once regarded as the pinnacle of human intelligence, and now she has been converted into 202,000 bits on a server.

In an era when truths no longer need to be mediated by humans, do we have the courage to follow the path taken by AI and explore the unknown areas beyond human intuition?

Sources

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 account "New Intelligence Yuan", author: Qing Qing, published by 36Kr with permission.