DeepMind AlphaProof Nexus gets peer reviewed in Science for solving open math problems
Google DeepMind's AlphaProof Nexus solved 9 of 353 Erdos problems and 44 OEIS conjectures with Lean-checked proofs. The work is now peer reviewed in Science.
Most AI math headlines still leave a quiet doubt in the room. A model writes a long answer that looks like a proof, a blog post celebrates it, and then a human expert has to check every line for a subtle mistake. That gap between "looks right" and "is right" is why research mathematics has been cautious about trusting language models on their own.
On October 8, 2026, that story took a clearer turn. The journal Science published a peer reviewed paper on AlphaProof Nexus, a Google DeepMind system that searches for proofs in the formal language Lean. Lean is not a chat box. It is a proof assistant. Every step has to type-check. If the logic is wrong, the compiler rejects it. That single property is the reason this result matters more than another leaderboard screenshot.
According to the AAAS EurekAlert release and DeepMind's public materials, AlphaProof Nexus solved nine of 353 attempted Erdos problems, including two that had stayed open for 56 years. It also proved 44 of 492 open conjectures drawn from the On-Line Encyclopedia of Integer Sequences. The Lean proofs are available in a public GitHub repository. Below is what the system actually does, what the numbers mean, and why the peer review step is as important as the scoreboard.
The three things you need to know
- What is new. Science published AlphaProof Nexus, a DeepMind framework that writes mathematical proofs in Lean and uses compiler feedback to reject fake logic. The work is peer reviewed, not only a blog post or an arXiv dump.
- The numbers. The system solved 9 of 353 attempted Erdos problems, including two open for 56 years, and 44 of 492 open OEIS conjectures that passed manual review for correct formalization.
- How it works. The agent is built around Gemini 3.1 Pro drafting and revising Lean proofs. For harder subproblems it can call AlphaProof, a specialized prover. DeepMind reports that even without AlphaProof it still solved those nine Erdos problems.
Why formal proofs change the conversation
Large language models are good at sounding correct. They are much worse at guaranteeing correctness. In ordinary prose, a missing case or a quiet swap of quantifiers can hide for days. In Lean, those mistakes usually fail immediately. The model proposes a proof. The compiler checks it. Error messages guide the next attempt. That loop is the heart of AlphaProof Nexus.
This is also why the Science publication lands in the middle of a heated debate about AI and mathematics. OpenAI recently released hundreds of AI generated math manuscripts on GitHub instead of sending them through journals. A group of mathematicians, including voices associated with the Association for Human Mathematics, pushed back hard on that approach. DeepMind took the slower path: formalize, verify, and put the work through peer review. You can disagree with the framing of either side and still see the difference in evidence quality.
Jeremy Avigad and Matthew Ballard, writing in a related Science Perspective summarized by EurekAlert, make a quieter but important point: even failed AI proof attempts can help mathematicians understand a problem better. The goal is not only to replace people. It is to give researchers a tool that fails loudly instead of failing politely.
What AlphaProof Nexus actually solved
The Erdos problems are a famous list of questions posed by Paul Erdos and later collaborators. Many are short to state and hard to settle. DeepMind's full featured agent attempted 353 formalized Erdos questions and solved nine of them autonomously. Coverage of the paper says two of those had been open for 56 years, dating back to questions posed around 1970 by Erdos and Sarkozy. Independent summaries list the solved formal subquestions, including variants of problems such as #12(i), #12(ii), #741(i) and #741(ii), with Lean files in the public results repository.
On the OEIS side, Gemini helped autoformalize 492 open conjectures about integer sequences. Before the agent could claim a conjecture, it had to prove test lemmas that checked the first terms of each sequence against the formal definition. That guardrail matters. A proof of the wrong statement is worse than no proof at all. After manual review, 44 conjectures were judged correctly formalized and previously unproven.
The paper and follow up reporting also mention other research level wins: an open question on Hilbert functions in algebraic geometry, an improved bound in convex optimization through a novel parameter schedule, help on problems linked to Ben Green's list, and ongoing work in quantum optics and graph theory. Those are not "AI did homework" stories. They are research adjacent claims, and they are the reason peer review and public Lean files matter.
DeepMind reports that the inference cost was on the order of a few hundred dollars per hard problem. That is not free, but it is cheap compared with months of specialist time. It also means labs without a seven figure budget can at least imagine running similar loops.
Gemini, Lean, and the optional AlphaProof tool
AlphaProof Nexus is not one magic model. It is a framework of agents that search for proofs with Lean feedback. The paper describes a basic generate and verify loop and a fuller agent that coordinates subagents, including through an evolutionary style search, and can call AlphaProof as a focused proof tool. AlphaProof itself is DeepMind's olympiad level Lean prover, known from earlier competition results.
The writing model in the loop is Gemini 3.1 Pro. It drafts a Lean proof, gets compiler errors, revises, and repeats. For harder subproblems the fuller agent can hand work to AlphaProof. One of the more interesting claims in the coverage is that a simpler generate and verify agent also solved the same nine Erdos problems in a post hoc check, sometimes at higher cost on the hardest ones. That suggests the breakthrough is less about a fancy controller and more about a strong model plus a ruthless checker.
That lesson travels outside math. Whenever an AI system can act in the world, you want an external check that does not trust the model's own confidence. Lean is that check for proofs. For code it might be tests and types. For agents it might be sandboxes and audited tools. The pattern is the same: do not let the model grade its own homework.
What this does not mean
It does not mean every open problem is about to fall. Nine of 353 is roughly 2.5 percent on that Erdos slice. Forty four of 492 is under 10 percent on the OEIS slice. Many of the solved items are formal subquestions or variants. Some critics of AI math work argue that formalization choices can make a problem easier than the informal statement mathematicians care about. DeepMind tried to reduce that risk with test lemmas and manual review, but readers should still treat the headline carefully.
It also does not settle credit. If an AI finds a Lean proof and a human checks the statement, who "solved" it? Journals, arXiv norms and prize committees will keep arguing about that. The Science paper does something useful either way: it puts the artifacts where other experts can inspect them.
Finally, peer review is not a halo. It is a filter. It means other researchers looked at the claims and methods and the journal chose to publish. It does not mean every interpretation in a press release is ironclad. Primary sources still win: the paper, the Lean files, and the EurekAlert summary from AAAS.
Why it matters
AI systems are moving from answering questions to claiming discoveries. That shift only works if outsiders can verify the claim without trusting the company blog. Formal proofs are one of the few domains where verification can be mechanical. AlphaProof Nexus shows a practical recipe: strong language models, a formal checker, public artifacts, and peer review.
For students and working mathematicians, the near term value may be more humble than "AI solved Erdos." It may be a tireless assistant that explores dead ends, finds misformalizations, and hands you a machine checked sketch you can rewrite in human language. For AI builders, the lesson is broader. If your system can be wrong in a way that looks right, you need a checker that cannot be talked into agreeing.
Dany's take
I am more convinced by a short Lean file than by a long confident essay. The industry spent years selling fluent answers. This result sells something rarer: answers that break when they are wrong. Nine problems out of hundreds is not a takeover of mathematics. It is a credible tool entering the lab notebook. If more labs publish machine checked proofs instead of screenshots of chat windows, the whole field gets easier to trust. That is the part I want to see copied.
Sources
Source: science.org