DeepMind AlphaProof Nexus Lands on *Science*: AI Independently Cracks Multiple 56-Year-Unsolved Erdős Mathematical Problems

Recently, the AI mathematics community has been full of dramatic developments. On October 6, OpenAI dumped 722 AI-generated mathematical manuscripts on GitHub at one go, which immediately caused a huge stir in the mathematics circle, and the Association of Human Mathematicians (AHM) led by Terence Tao issued a statement calling for a boycott.

In the same week, a paper from Google DeepMind was published in Science on October 8, having gone through the formal peer review process.

According to media reports, the protagonist of this paper is AlphaProof Nexus, an automatic system for discovering mathematical proofs. Its achievement is that among 353 unsolved Erdős problems, it independently solved 9 of them, 2 of which have been pending since 1970 for 56 years.

Paper link: https://www.science.org/doi/10.1126/science.aej2213

The Erdős problems are a set of open problems named after the Hungarian mathematician Paul Erdős, mostly distributed in combinatorics and number theory. He also liked to post clear monetary rewards for difficult problems during his lifetime. This set of problems has now become the touchstone for testing the mathematical capabilities of AI.

There is a detail that none of these 353 problems are easy targets selected by DeepMind itself. They are all the Erdős problems that have been translated into the Lean language in the Formal Conjectures repository of the open source community (as of February 2026). The system processes all of them, attempting at most 3000 rounds for each problem and giving up if it cannot produce a proof. The 9 problems it finally solved include the 12th problem proposed by Erdős and Sárközy in 1970.

The transcript does not end here: among the open conjectures in the OEIS Encyclopedia of Integer Sequences, 44 out of 492 have been proven; a 15-year-old unsolved algebraic geometry problem (the conjecture about Hilbert functions) has been solved; an unthought-of parameter adjustment scheme has been found in min-max optimization, which improves the known upper bound. In addition, it also helped tackle an open problem on the list of mathematician Ben Green, and is now being used to support ongoing research projects in quantum optics and graph theory.

In terms of cost, the figure given in the paper is an inference overhead of several hundred dollars per problem.

How it produces proofs

The core loop can be explained in one sentence: the large model is responsible for writing, and the compiler is responsible for judging.

Specifically, Gemini 3.1 Pro uses the formal language Lean to draft proofs. After each revision, the Lean compiler checks line by line, and the error message is fed back to guide the next draft. The system also has several safeguards: no changes are allowed to the theorem statements, no "sorry" placeholders are allowed in the proof, no additional axioms are allowed, and the entire verification runs in a sandbox.

On top of this loop, the research team also built an "evolution" framework: a group of sub-agents search for proofs independently, compete with each other in tournaments using an Elo rating similar to that in chess, retain promising ideas and discard dead ends; when encountering hard sub-problems, they can call AlphaProof, the dedicated prover that reached the silver medal level of the International Mathematical Olympiad in 2024.

Workflow of AlphaProof Nexus: Mathematicians provide natural language background, Lean formalized problems and knowledge base. The internal proof sub-agents, review sub-agents and verifier of the system iterate around a "population database" to finally output formal proofs.

However, there is a very practical ablation result in the paper: after removing the fancy framework and only retaining the simplified version of the system of "large model plus Lean feedback", all 9 Erdős problems can still be solved, only the most difficult ones cost more. In other words, the main contributor is the combination of the base model and compiler feedback itself.

Problem solving rate and average cost on 6 Erdős problems. The blue line is the simplified system, the orange line is the version added with AlphaProof, and the red triangle is the complete system. The solving cost of most problems is between tens to hundreds of dollars.

A few words of caution

First, the hit rate. 9 out of 353, which is about 2.5%. This ratio is basically consistent with Terence Tao's estimate that "the success rate of AI solving Erdős problems is roughly 1% to 2". The vast majority of open problems are still out of its reach. The paper itself also admits that the successes are concentrated in fields where the Lean mathematical library is relatively mature, and problems that require a large number of new theories are not yet achievable.

Second, the number of solved problems may be overstated. After the paper made all the Lean proofs public, an independent audit found that although the proof of Problem 846 is valid, a theorem from Reiher, Rödl and Sales in earlier years actually already implies the answer. According to the stricter definition of "newly solved", the number 9 should be changed to 8. In addition, Problems 741 and 846 were also independently solved by OpenAI's internal model.

Third, the system is not open. The proof files are available for download on GitHub, but AlphaProof Nexus itself is not accessible to the public, so others cannot reproduce it personally. DeepMind CEO Hassabis also stated early on that this is still not AGI.

The timing and method of publication are thought-provoking.

On October 6, OpenAI uploaded 722 manuscripts covering 372 result series to GitHub, claiming that it referred to the suggestions of the independent advisory group of the Institute for Advanced Study in Princeton. As a result, 3 of them were withdrawn within one day due to symbolic errors.

AHM, chaired by Terence Tao, then issued a statement criticizing this as a demonstration of force and calling on mathematicians to boycott. On October 9, Terence Tao reposted the column article by mathematician Thomas Hales on his personal blog, Lean Theorem Provers That Mathematicians Should Know About: Reliability and Artificial Intelligence Issues.

As for DeepMind, it first posted the preprint on May 21, then made the solutions public in advance on the ErdosProblems forum for experts to review and spot errors, and finally submitted the paper to the peer review process of Science. The Lean proofs of those 9 problems have also been registered on the wiki page "AI Contributions to Erdős Problems" maintained by Terence Tao long ago.

This article is from the WeChat Official Account "Big Data Digest", and is published by 36Kr with authorization.