A research paper on Google DeepMind's mathematical research AI, AlphaProof Nexus, was published in the journal Science on October 8, 2026. According to an announcement from the American Association for the Advancement of Science (AAAS), the research team found computer-verifiable proofs for 9 of 353 open "Erdős problems" and 44 of 492 open conjectures listed in the integer-sequence database OEIS. The Erdős results include two questions that had gone unsolved for 56 years, since they were posed in 1970. AI problem-solving in mathematics is moving beyond competition problems such as those in math olympiads, toward discovering proofs of open problems in actual mathematical research.
The results were not first announced in October, however. The paper by George Tsoukalas and colleagues was released on arXiv on May 21 and revised on June 8. What is new is that the research has now passed peer review and appeared in an academic journal. To understand the significance of the results, it is not enough to look at the number of problems solved. We also need to check which problems were targeted, how far the AI-generated proofs could be verified mechanically, and what role human mathematicians played.
9 Erdős Problems and 44 OEIS Conjectures Proved: What Do the Success Rates Mean?
The 353 Erdős problems that AlphaProof Nexus tackled were not randomly selected from all open problems in mathematics.
According to Section 3 and Appendix B.2 of the paper, as of early February 2026 the team evaluated all 353 Erdős problems that had been written in Lean in the open-source project "Formal Conjectures."
Lean is a proof assistant that lets users write mathematical statements and proofs in a formal language and have a computer verify their logical correctness. In this study, if the AI could not find a proof, the search was cut off after a maximum of 3,000 episodes. An episode here means a sequence of interactions in which the AI drafts a proof and revises it over multiple rounds.
For the conjectures in OEIS (On-Line Encyclopedia of Integer Sequences), the selection method was different.
The team first collected 2,649 open conjectures from OEIS, which catalogs integer sequences and their mathematical properties. Then it had Gemini choose 500. The criteria were that the conjectures be mathematically interesting and not easy to solve, yet avoid famous open problems and be considered suitable for automated proof.
Of the 500 selected, 8 that could no longer be run because of a Lean version update were excluded, leaving 492 for evaluation.
| Evaluation target | Problems attempted | Proofs found | How targets were selected |
|---|---|---|---|
| Erdős problems | 353 | 9 | All problems formalized in Lean as of early February 2026 were evaluated |
| Open OEIS conjectures | 492 | 44 | Gemini picked 500 from 2,649; 8 that could not be run were excluded |
The success rates work out to about 2.5% (9 ÷ 353) for the Erdős problems and about 8.9% (44 ÷ 492) for the OEIS conjectures.
However, these figures cannot be taken as "the probability that AI can solve an open math problem." The Erdős problems are biased in that the targets were limited to problems already formalized in Lean. For OEIS, problems suited to automated proof were selected on top of that.
In addition, the nine reported solutions include statements derived from the original problems and multiple sub-questions under the same problem number. This does not mean that nine independent, famous open problems were each fully solved in their original form.
Still, the fact that AI found formal proofs for problems that had stood open in actual research is a significant achievement.
Two Questions Unsolved for 56 Years Resolved
The most notable results are two questions that had been open since 1970.
Both are part of Erdős Problem 12, posed by the mathematicians Paul Erdős and András Sárközy.
The problem asks how many numbers can be gathered in a set of integers while avoiding a particular divisibility relationship.
For example, suppose a set contains 3, 7, and 8. The sum of 7 and 8 is 15, which is divisible by the smaller number, 3.
Problem 12 requires that such relationships not occur. That is, when any three distinct numbers are chosen from the set, the smallest must never divide the sum of the other two.
The first question asked whether it is possible to construct an infinite set satisfying this constraint such that the number of its elements from 1 to N stays at a size proportional to the square root of N.
AlphaProof Nexus found a method of dividing numbers into small groups, placing them sufficiently far apart, and combining them infinitely.
The proof combines the Chinese remainder theorem, which coordinates remainders after division by different primes, with a construction of sets containing no arithmetic progression of length 3. This shows that the required abundance of numbers can be secured while avoiding the divisibility relationship.
The second question was also resolved, by constructing sets with even more elements. Problem 12 contains other questions as well, however, so the problem as a whole has not been completely solved.
Another example that makes the results easier to grasp is Erdős Problem 125.
This problem considers a set A of non-negative integers that use only the digits 0 and 1 when written in base 3, and a set B of non-negative integers that use only 0 and 1 when written in base 4.
If you pick one number from each set and add them, you get a variety of integers. The question is whether the numbers obtained this way continue to make up at least a certain proportion of all integers.
The proof found by the AI answered that question in the negative.
Specifically, it showed that the "lower density" of the set of obtainable numbers is zero. Lower density is a measure of the lower-bound behavior, as N grows, of the proportion of integers from 1 to N that belong to the set.
A lower density of zero means that, as N increases, ranges appear in which the proportion of obtainable numbers becomes arbitrarily small. It does not, however, mean that the proportion approaches zero uniformly across all large ranges.
The proof exploits the fact that powers of 3 and powers of 4 can sometimes be very close in value, and it reaches its conclusion by repeatedly analyzing the distribution of numbers at different scales.
Gemini Devises Proofs, Lean Verifies Them
At the core of AlphaProof Nexus is a loop that alternates between proof generation by a large language model and formal verification by Lean.
According to Section 2 of the paper, in the basic configuration Gemini 3.1 Pro devises a proof strategy and writes code in Lean. That code is checked by Lean, and if errors appear, the AI uses their contents to revise the proof draft.
The input is a Lean file describing the statement to be proved and the necessary definitions. Parts of the proof that are not yet complete are marked with a special keyword, sorry.
sorry is a mechanism in Lean for temporarily leaving a part unproved. The AI's job is to replace these unproved parts with actual proofs so that every logical step can be verified by Lean.
Every time the AI changes the code, Lean checks it, and if verification fails it returns an error message. Using that information, the AI tries different proof strategies or adds lemmas as it continues its search.
Even if a proof is not completed in a single attempt, the methods tried so far and the remaining challenges are recorded and carried over to the next attempt.
In the basic configuration, multiple proof-search agents search for proofs independently, without sharing state with one another.
In the extended configuration, by contrast, partially completed proof drafts are accumulated in a shared database so that other agents can pick them up and improve them.
In addition, Gemini 3.0 Flash is used as an evaluation model to compare multiple proof drafts on criteria such as how clear the proof strategy is, how likely the unproved parts are to be resolved, and how novel the ideas are.
The evaluation results are quantified using the Elo rating system, also used to rate strength in chess and other games, and serve as input for deciding which proof draft to explore next.
Such an evaluation model is needed because completed proofs and unfinished drafts are assessed differently.
A completed proof can have its logical correctness verified by Lean. For an unfinished draft, however, one must judge not only whether it is correct at present but also whether further exploration is likely to complete it.
That said, a high ranking from the evaluation model does not guarantee that a proof draft is correct. The evaluation model only sets search priorities; the final correctness of a proof is confirmed by Lean.
The extended configuration can also delegate parts of a proof to a specialized proof system, "AlphaProof."
Given a subproblem, AlphaProof returns a proof if it finds one, or shows that the statement does not hold if it finds a counterexample. If it obtains neither, it reports that it could not solve the subproblem.
By having Gemini devise the overall structure of a proof and handing the difficult parts to a specialized tool, the system achieves a search that combines multiple methods.
Machine Acceptance of a Proof Doesn't Always Mean the Original Problem Is Solved
An important point in using formal verification is whether a proof that Lean accepts as correct is really an answer to the original mathematical problem.
In Lean, code can pass type checking even if sorry remains in unproved parts. That does not mean the proof is complete.
For this reason, AlphaProof Nexus requires that no sorry remain in the final proof.
It also uses a verification tool, SafeVerify, to check whether the original statement has been improperly altered and whether any unauthorized axioms have been added.
This is to prevent the AI from creating an appearance of success by assuming parts it cannot prove to be true, or by rewriting the statement to be proved into an easier one.
Even these safeguards, however, cannot solve one problem: whether a mathematical problem written in natural language was correctly translated into Lean's formal language in the first place.
What Lean verifies is only a proof of a statement written in the formal language. Whether that statement matches the problem mathematicians actually meant to solve must be confirmed separately.
The research team explains that each time a proof of an Erdős problem succeeded, an in-team mathematics expert compared the original problem text with the formalized statement and confirmed that the two matched.
For the OEIS conjectures as well, the AI was first made to prove "test lemmas" showing that the first several terms of the sequence are correctly reproduced from the formalized definition.
For the 44 conjectures whose proofs then succeeded, humans confirmed that the formalization was correct and that the conjectures had previously been unproved.
Of course, matching the first few terms of a sequence does not guarantee that the whole conjecture has been formalized correctly. That is why machine pre-verification is combined with confirmation by experts.
In fact, for parts of Erdős Problems 125 and 741, the interpretation of the word "density" in the original problem text had to be corrected.
Statements that had initially been treated with ordinary natural density were revised to lower density and upper density, respectively, and proofs were obtained for the revised statements as well.
The public catalog entry for Problem 125 also records how the meaning of density had been ambiguous in earlier literature.
This case shows the importance of clarifying what should be proved in the first place, not just finding a formally correct proof.
The study also analyzed cases in which the AI failed to produce a proof.
For example, in some cases the AI moved the difficult core of a problem into a lemma that was only a slight rewording of the original statement, and left that lemma as sorry.
There was also an example in which humans investigated a lemma the AI claimed was "already proved in the mathematical literature" and found that it was actually a nonexistent theorem.
In other words, building in formal verification does not eliminate hallucinations, the generation of plausible but false information, by generative AI.
The strength of formal verification is that even if the AI brings up faulty reasoning or fictitious theorems along the way, an unfinished proof built on them is not accepted as complete.
Nine Proofs Without Complex Machinery, at a Cost of Hundreds of Dollars per Problem
The study also contains an interesting result about the design of AI proof-search systems.
For the nine Erdős problems solved by the advanced AlphaProof Nexus configuration, the research team later ran comparison experiments with the basic configuration.
The result was that the basic configuration, without proof-draft sharing, evolutionary search, or integration with AlphaProof, could also prove all nine of the same problems.
In other words, a relatively simple setup, in which a general-purpose large language model generates proofs and repeats cycles of Lean verification and revision, was shown to be capable of handling open problems at the research level.
However, this comparison was run after the fact, on the nine problems that the advanced configuration had already solved. It does not show that using the basic configuration to search all 353 problems anew would have produced the same results.
Nor can it be concluded that complex configurations are unnecessary.
According to Section 5 of the paper, for the difficult Problems 125 and 138, the advanced configuration combining evolutionary search and AlphaProof was 2 to 5 times more cost-efficient than the basic configuration and others.
For the other problems, on the other hand, the advanced configuration's cost efficiency was roughly half.
Managing a database for sharing proof drafts and ranking them with an evaluation model also requires computational resources, so making the system more complex does not necessarily raise efficiency.
Simple configurations may be advantageous for relatively easy problems, while combining multiple search methods may become more valuable for hard problems.
This result suggests that, in improving the performance of mathematical research AI, what matters is not only the capability of specialized models but also what problems are given to a general-purpose model and how feedback from the verifier is used.
The authors also cite improvements in the capabilities of the large language models themselves and the usefulness of Lean's error messages as reasons for the strong performance of the basic configuration.
The reported cost of "hundreds of dollars per problem" in this study, meanwhile, needs careful interpretation.
This figure is not the total cost required to take a problem from discovery to solution. The research team searched the 353 Erdős problems broadly, and just finding provable problems among them consumed considerable computational resources.
In addition, the comparative costs shown in Figure 3 of the paper do not include the inference cost of AlphaProof itself.
The authors estimate that AlphaProof costs about 27.5 TPU-hours per problem, or about $60.
AI search also varies considerably from run to run, and the amount of computation needed before a proof is found is not constant even for the same problem.
Therefore, the figure should not be taken to mean that you can solve open problems for a few hundred dollars, or that any math problem you bring in will be solved at that price. Nor can it be used for a simple comparison with the research costs of human mathematicians.
Applications to Mathematical Research Extend to Optimization Theory and Algebraic Geometry
The results of AlphaProof Nexus are not limited to Erdős problems and OEIS conjectures.
The research team has also used the system in actual mathematical research in areas such as optimization theory, algebraic geometry, and graph theory.
In optimization theory, it obtained a new result guaranteeing convergence performance for an algorithm called "Anchored Gradient Descent-Ascent," which solves min-max problems with convex-concave structure.
This is an optimization problem involving two opposing operations: minimizing the objective function over one variable and maximizing it over the other.
The research team allowed the AI to modify the parameters that determine the algorithm's update step size, and had it explore which settings would yield stronger convergence guarantees.
As a result, it proved an exact O(1/t) convergence rate for the squared gradient norm at the last iterate. Here t denotes the number of iterations, and O(1/t) indicates how small the upper bound on the squared gradient norm becomes as the number of iterations grows.
What matters is that the AI did not merely confirm the correctness of an algorithm prepared by humans.
The AI itself searched for parameter settings that would yield stronger guarantees, and even proved that the algorithm converges with those settings.
An independent preprint on this result was also released in April.
However, an improved theoretical convergence guarantee does not mean that the training speed of actual large-scale AI models has improved. The result was obtained under specific conditions, smooth convex-concave problems, and does not measure any speedup when applied to real AI training.
In algebraic geometry as well, the AI found new proofs.
The subject was a problem concerning sequences called "pure O-sequences," and it proved that "log-concavity" holds under the specific conditions of codimension 3 and type 2.
Log-concavity is the property that, for any three adjacent terms of a sequence, the square of the middle term is at least the product of its two neighbors.
This condition is stronger than "unimodality," the property that a sequence increases up to a point and then decreases. The proof thus yields a result stronger than the already-known unimodality.
However, log-concavity was not proved for all pure O-sequences; the scope is limited to cases satisfying specific conditions.
In graph theory, too, a result related to the long-studied "graph reconstruction conjecture" was reported.
The graph reconstruction conjecture asks whether an original graph can be recovered from information about the subgraphs obtained by removing its vertices one at a time.
The team focused on "bipartite graphs," in which vertices are divided into two groups and no edges connect vertices within the same group, and proved that a proposed reconstruction algorithm works correctly when certain additional conditions are satisfied.
The statement for general bipartite graphs without the additional conditions remains open.
These results show that AI-driven proof search is spreading across multiple areas of mathematics. However, they do not resolve the open problems of whole fields, and as shown in Section 4 of the paper, each has clear limits on the scope and conditions of the proof.
Can Mathematicians Verify the Published Proofs and Build on Them?
Google DeepMind provides the proofs generated by AlphaProof Nexus in a public GitHub repository.
The repository contains formal proofs written in Lean and natural-language explanations of their content that are easier for humans to understand. Build instructions for verifying the proofs in a Lean environment are also published.
This allows third-party researchers to examine the published proofs themselves rather than simply accepting DeepMind's report of success.
Still, there are several points to check here as well.
First, what Lean and SafeVerify confirm is whether the proof of a statement written in the formal language holds logically, and whether any improper changes were made during the proof process.
Second, human mathematicians need to confirm whether that statement correctly represents the original mathematical problem.
Third, through peer review and post-publication discussion, the validity of the research methods, the novelty of the results, and their significance for existing mathematical research are evaluated.
Formal verification by machine, human judgment about what a problem means, and academic evaluation as a research result each play a different role.
Also, the fact that completed proofs are public is not the same as anyone being able to reproduce the search process that arrived at them.
The study provides a means of verifying completed proofs, but it does not guarantee that a third party can run the same search and obtain the same results at the same cost.
The research team itself acknowledges that the current system has clear limitations.
The successes so far are concentrated in fields where Lean's mathematics libraries are relatively well developed, such as combinatorics, convex optimization, and number theory. Problems that require building large new mathematical theories, or where even formalizing existing definitions and theorems takes enormous effort, remain difficult to handle.
Nevertheless, it has already been shown that proofs and intermediate results produced by AI can be useful for human mathematicians' research.
For example, the public catalog entry for Erdős Problem 12 records that the proofs found by DeepMind were later simplified and improved through discussion among mathematicians.
Mathematicians on the research team also report that even when the AI could not complete a final proof, the partial drafts it produced deepened their understanding of the problem's structure and let them focus their efforts on the remaining difficult parts.
This point is important when thinking about the future of AI in mathematical research.
In mathematical research, value lies not only in proving that a statement is true but also in understanding why the proof works, finding simpler methods, and applying them to other problems.
The results of AlphaProof Nexus show that AI can find formal proofs of open problems, and at the same time make clear that human understanding and verification remain essential for establishing those results as mathematical knowledge.
Going forward, what will matter is not only increasing the number of problems that can be solved, but also how well third parties can understand discovered proofs, simplify them, and develop them into other research.
AI finds the proof, machines verify its correctness, and humans interpret its mathematical meaning and carry it into the next piece of research. AlphaProof Nexus shows that this kind of human–AI collaboration in mathematical research is already beginning to produce real results.