AI cracks a 56-year-old mathematical problem and the related research is published in *Science*. DeepMind takes the proper approach by submitting its findings for peer review.

The AI mathematics community has been exceptionally lively recently.

Shortly after OpenAI released 722 mathematical proofs in one go and faced collective pushback from the mathematics community, Google DeepMind's mathematical research was published in Science.

One party bulk released manuscripts pending verification, shifting the heavy burden of proofreading to mathematicians;

The other waited steadily for several months, went through the full peer review process properly, and accepted the scrutiny of the mathematics community.

Two mathematicians from Carnegie Mellon University and the University of South Carolina specifically wrote a commentary in the same issue of *Science* titled: *AI for Mathematical Research Has Arrived*.

Well, while OpenAI is still caught in heated disputes over the way of publishing mathematical proofs, DeepMind has already received public recognition from mathematicians.

The protagonist of DeepMind this time is AlphaProof Nexus, an AI mathematical proof Agent framework driven by Gemini.

It has solved 9 Erdős open problems, two of which had remained unsolved for a full 56 years.

Apart from these 9 problems, it has also proven 44 conjectures in the OEIS Encyclopedia of Integer Sequences, solved a 15-year-old unsolved algebraic geometry problem, and improved a long-established theoretical boundary in the field of convex optimization.

Speaking of which, DeepMind is no stranger to *Science*.

This mathematical paper has 20 authors in total, among whom Aja Huang was also a core researcher back when AlphaGo was developed.

Breaking Through the 56-Year-Old Prize Problem

DeepMind selected 353 problems from existing Lean formalized versions, assigned them to AlphaProof Nexus for attempts, and finally successfully solved 9 of them.

Among them, Erdős #12 was proposed in 1970 and has remained unsolved for 56 years up to now.

The question goes as follows:

Is it possible to find an infinite set of integers where the numbers in the set satisfy strict divisibility restrictions while remaining sufficiently large in scale?

Specifically, for any three eligible integers selected from the set, the smaller one cannot divide the sum of the other two larger integers, and the set cannot be too sparse.

Since 1970, no one has been able to give a complete construction of this set. There have been various partial advances, but they could never be combined into a full solution.

The solution adopted by AlphaProof Nexus this time is block-based construction.

First, split the infinite set to be constructed into individual integer blocks;

Then use the Chinese Remainder Theorem, combined with the properties of sets that avoid 3-term arithmetic progressions, to make each block satisfy the local divisibility conditions;

Finally, piece all the blocks back together to form a complete infinite set.

In addition, there is Erdős #125, which was proposed in 1996 and had no conclusion for 30 years.

Imagine two sets of numbers:

The first set consists entirely of "integers that contain only the digits 0 and 1 in base 3";

The second set consists entirely of "integers that contain only the digits 0 and 1 in base 4";

Add all pairs of numbers from these two sets to get a new set.

The question is: Is the frequency (mathematically called lower density) of the numbers in this new set among natural numbers positive?

Intuitively, you may think that the numbers contained in the two original sets are not that many, so their sum set should also be quite sparse.

But how sparse is it exactly? Is it sparse enough that the density drops to zero, or does it maintain some positive density?

The difference between these two outcomes is extremely subtle, and there was no definite conclusion after the problem was proposed in 1996.

The answer given by AlphaProof Nexus is: The lower density is zero.

The key to the proof lies in the fact that log₄/log₃ is an irrational number.

This means that powers of 3 and powers of 4 can be arbitrarily close to each other at appropriate scales.

Using this property, the AI constructed an inductive sparsification argument: it continuously finds two almost aligned scales to make the set density decay step by step until it drops to zero completely.

It finally proved that the lower density of this set is indeed zero.

Erdős #846, proposed in 1992, had stumped humans for 34 years.

This is a problem about planar point sets.

Is it possible to construct an infinite planar point set with a very peculiar property:

For any finite number of points selected from it, you can find a sufficiently large subset with no three points collinear.

But if you try to split the entire infinite point set into a finite number of sets that have no three collinear points at all, it is impossible to do so.

To put it simply, the set looks quite regular locally, but you can never split it completely to meet the requirement as a whole.

The proof given by AlphaProof Nexus uses a clever mathematical construction.

It maps the edges of an infinite complete graph to points on the plane, encodes the coordinates with polynomial expressions, and then combines relevant conclusions from infinite combinatorics to complete the proof.

A plane geometry problem was finally solved by converting it into a graph theory and combinatorics problem.

Apart from these three problems, the remaining six are in the fields of divisibility set construction, Van der Waerden number gaps, Sidon set isolated points, set splitting density and other domains.

After finishing the Erdős problems, it went on to prove 44 open conjectures in the OEIS Encyclopedia of Integer Sequences.

It did not leave out algebraic geometry and convex optimization either.

It solved a 15-year-old unsolved case about the log-concavity of Hilbert functions in algebraic geometry, and improved the theoretical boundary of an anchored gradient descent method in the field of convex optimization.

Gemini Writes Proofs, Lean Grades Them

The core working mechanism of AlphaProof Nexus is:

Gemini 3.1 Pro writes the proof → Lean checks it → Error reports are fed back to Gemini → Modify the proof → Check again, until the entire proof passes verification.

Around this workflow, DeepMind designed four Agent configurations.

The simplest Agent A is multiple independent sub-Agents attempting to prove problems simultaneously.

Each sub-Agent generates Lean code via Gemini, and keeps modifying it based on feedback from the compiler.

There are no additional auxiliary tools throughout the whole process, it purely relies on the loop of writing code and debugging errors.

Agent B adds AlphaProof.

It is a dedicated mathematical proof system previously developed by DeepMind.

When encountering hard-to-solve sub-problems, the Agent can call AlphaProof for targeted search.

Agent C introduces evolutionary search.

Multiple Agents put different proof drafts into a shared database, then a scoring Agent based on Gemini 3.0 Flash compares the rationality, clarity and novelty of the drafts.

The system aggregates the comparison results into Elo ratings, and then selects the proof routes worthy of further exploration based on these ratings.

Agent D is the full version.

It integrates both AlphaProof and evolutionary search, and is also the main configuration used in this batch exploration of open problems.

Theoretically, the more functions a configuration has, the more powerful it should be.

But later DeepMind ran a set of controlled experiments and found that the simplest Agent A could actually solve all 9 Erdős problems.

Without evolutionary algorithms and without AlphaProof, Agent A, which only uses the LLM loop plus compiler feedback, just costs more money on difficult problems.

On difficult problems such as #125 and #138, the full version Agent is about 2 to 5 times higher in cost efficiency than the basic version.

Overall, the cost for AlphaProof Nexus to solve one problem this time is roughly several hundred dollars...

The full set of Lean proof code from this project has been made public, and the public can view it directly.

Speaking of which, Erdős himself once set cash bounties for many difficult mathematical problems during his lifetime, encouraging mathematicians all over the world to challenge them.

Nowadays, besides the wisdom of mathematicians, computing power has also begun to become the key to unlocking these bounty problems.

This article is from the WeChat Official Account QbitAI, author: Focus on cutting-edge technology, published with authorization from 36Kr.