AlphaProof Nexus Deep Dive: When Code Proves Theorems — Three Hundred Dollars a Problem, Fifty-Six Years of Waiting

| Paper Info | | |---|---| | Title | Advancing Mathematics Research with AI-Driven Formal Proof Search | | Authors | George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferrauiolo, Henryk Michalewski, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri (20 authors) | | Institutions | Google DeepMind, Aarhus University | | arXiv ID | 2605.22763 | | Date | May 21, 2026 | | Category | cs.AI | | Code | github.com/google-deepmind/alphaproof-nexus-results | | Core claim | Using LLMs to generate Lean-formalized proofs, the first large-scale demonstration that AI can solve open mathematical problems — independently solving 9 of 353 Erdős problems, at a cost of only a few hundred dollars each |

---

In 1996, Paul Erdős posed a problem. The wandering mathematician of the field — who proposed over 1,500 open problems in his lifetime — called any tough mathematical nut "worth paying for." Some problems were worth $25, some $1,000. He never got to price #125. That problem lived on for 30 years, unsolved.

In spring 2026, a machine finished it in a few hours. Cost: under $300.

The problem: let A be the set of ternary numbers written only with the digits 0 and 1 (e.g., 10, 101, 1101). Let B be the set of quaternary numbers written only with 0 and 1. Is the sumset A+B — all pairwise sums — "dense" enough? Plainly: is it true that for all sufficiently large N, the count of elements of A+B below N, divided by N, stays above some positive constant?

Three sentences, describing a 30-year-old open problem. The machine's answer, as you might guess — no. The density is zero. The proof is elegant: using Diophantine approximation of \(3^m \approx 4^k\), it constructs an inductive "thinning" argument, peeling away impossible elements layer by layer.

This was no isolated case. The same machine solved eight other Erdős problems on the same day.

---

🧮 A Reasoning Engine That Can't Tell True from False

First, why is this hard?

LLMs doing mathematical reasoning have a fatal flaw: you don't know which sentences are right and which are wrong. Ask it to prove a theorem and it may write ten steps, nine correct, and in the tenth step fabricate a lemma out of thin air — a lemma that happens to be false. Yet the argument reads flawlessly.

The mathematical community takes this extremely seriously. A paper gets published only after reviewers spend months checking line by line. A major theorem may be cross-verified by multiple mathematicians. This is not superstition — experience has taught them that human brains doing long-chain reasoning do make mistakes. LLMs err at rates and in ways even harder to predict.

Could we skip having humans check?

Yes. Use the compiler.

Lean is a formal proof language. Writing a proof in Lean is like writing a program. Lean's compiler verifies line by line and errors on any missing logical step. Compilation succeeds = the proof is correct. There is no middle ground.

AlphaProof Nexus — Google DeepMind's system — does one thing: puts the LLM inside a Lean compiler cage, lets it generate proof drafts, verifies them on the spot, rejects and rewrites errors, and only accepts what compiles.

You can also think of it this way: the LLM does the "thinking," Lean does the "judging." Wrong thinking means thinking again. Correct thinking passes. They alternate until the proof is done.

---

🏗️ Two Agents, One Iron Rule

Two kinds of agents live inside AlphaProof Nexus.

Basic (Agent A): Minimal. Feed the problem to Gemini 3.1 Pro, the model generates a proof draft, Lean compiles it. On errors, the model reads the error messages, revises, recompiles. Loop. N independent "proof sub-agents" run simultaneously — first to succeed wins.

Full (Agent D): Three modules stacked on the basic version.

The first is AlphaProof — DeepMind's earlier formal proof engine developed for mathematical olympiads. When a sub-agent gets stuck mid-proof, it can toss a subgoal to AlphaProof: "prove this for me." AlphaProof returns one of three outcomes: proof succeeded, disproved (the subgoal is false), or couldn't handle it.

The second is evolutionary search. Each round's proof sketches (compiling "half-finished" products with sorry remnants) are stored in a population database. Gemini 3.0 Flash acts as peer reviewer — sampling 7 sketches at a batch and ranking them by clarity, feasibility, and mathematical novelty. Higher-ranked sketches earn higher Elo scores and greater probability of being selected to "breed" in the next round.

The third is a global goal cache. If a subgoal has already been settled by AlphaProof for some sketch, other sketches can reuse that result without recomputing.

The whole pipeline is one giant parallel search — hundreds of "proof writers" scribbling on scratch paper simultaneously, with the compiler as a never-sleeping referee.

---

📊 Nine Problems, Three Hundred Bucks Each

The paper's system evaluation runs along two tracks.

Track one: Erdős problems.

From the "Formal Conjectures" repository, 353 currently formalized open Erdős problems were selected and all fed to the full agent. Each problem ran up to 3,000 rounds. Nine were proven.

The nine problems span number theory, combinatorics, and additive combinatorics. Two date from 1968 — 56 years old. One from 1996 — 30 years. Another, posed not by Erdős himself but classified under his umbrella, was also solved.

Inference cost per problem: a few hundred dollars (mostly Gemini 3.1 Pro API fees; AlphaProof adds about $60 per problem on TPUs).

All proofs are explicitly public, and the results have been recorded in Terence Tao's "AI contributions to Erdős problems" wiki.

Track two: OEIS conjectures.

OEIS is the Online Encyclopedia of Integer Sequences. The paper used Gemini to automatically formalize 492 unresolved OEIS conjectures into Lean statements, then fed them to the agent. Result: 44 were proven — human-verified as correctly formalized and never previously proven.

Two examples appear in the supplementary material. One involves a modular property of sequence A000045, dispatched in one stroke by induction; the other ties a combinatorial generating function to a recurrence relation, cleanly executed.

---

🔬 In the Field: From Optimization to Quantum Optics

The paper's ambitions overflow the benchmark. The authors deployed the system in real mathematical research.

Convex optimization. The agent resolved an open convergence-rate question: proving that anchored gradient descent-ascent (GDA) achieves an exact \(\mathcal{O}(1/t)\) convergence rate in minimax convex-concave optimization, tightening looser upper bounds from prior work. The most delightful part — the agent not only proved the rate, it autonomously discovered a new parameter schedule. Humans gave it a tunable parameter marked EVOLVE-VALUE; it searched the parameter space and found the optimal value making the proof work.

Algebraic geometry. A log-concavity question about Hilbert functions, open for about 15 years in codimension 3, type 2, was proven by the agent. The argument is substantial — requiring nontrivial reconstruction of the Hilbert function and case-by-case decomposition of second-difference inequalities.

Graph theory. Of two bipartite variants of the reconstruction conjecture, the agent proved one. A Graffiti conjecture on upper bounds for leaf counts in spanning trees (generated by an automated conjecturing system in 1996) was also proven.

Additive combinatorics. Problem #57 from Ben Green's famous open-problem list — on the equivalence of two spaces of quadratic functions — the agent could not prove directly. But it did something smarter: using floating-point heuristic search, it found a counterexample (the cyclic group \(\mathbb{Z}/3\mathbb{Z}\)), then proved that this counterexample indeed refutes the original conjecture. A variant of the problem was disproven; an independent paper is being written.

Quantum optics. Collaborating with Mario Krenn, the agent solved multiple conjectures on the existence of monochromatic quantum graphs — the cases \(N=d \in \{4,6,10\}\) were all conquered; another paper is in the works.

---

⚡ Unexpected Docility: Is the Basic Version Enough?

The most sobering data in the paper sits in the ablation experiments.

Via post-hoc analysis, the authors pulled the basic version (Agent A), the AlphaProof-augmented version (Agent B), the evolution-augmented version (Agent C), and the full version (Agent D) back onto those nine solved Erdős problems, and re-ran comparisons.

The result stunned. The basic version solved all nine. The difference from the full version isn't "can it solve it" but "how much does it cost." On easy problems the basic version is cheaper; on hard bones like #125 and #138, the full version cut inference cost to 1/2 to 1/5.

Another set of data: swapping Gemini 3.1 Pro for the smaller Gemini 3.0 Flash or Gemini 3.1 Flash-Lite, and running AlphaProof alone in tree-search mode — all drew blanks.

What does this mean? LLM + compiler feedback — a loop so simple it can't get simpler — can already, at current model capability levels, attack research-grade mathematics. Evolutionary search, AlphaProof augmentation, population databases — these nice-to-have components may sharply drop in importance over the next two years as LLM capability continues to grow.

This is the paper's sharpest observation: the center of gravity of AI mathematics is sliding from "train a dedicated problem-solving system" toward "use a sufficiently smart general model, paired with a compiler that never lies."

---

❓ The Honest Part: What Remains Unresolved

Having read all 35 pages, there are things I genuinely don't know the answers to.

Of 353 problems, 9 were solved — why not the other 344? The paper includes a failure analysis. The most lethal failure mode: the agent quietly stuffs the problem's core difficulty into an auxiliary lemma, then marks that lemma with sorry, pretending it "is a known result in the literature." LLMs under pressure fabricate lemmas — and fabricate them convincingly. The paper says the prompts explicitly forbid this behavior. It didn't help. This is an unrepaired crack between formal methods and LLM unreliability.

The cost has water in it. The paper's "a few hundred dollars per problem" only counts inference cost on successfully solved problems. But to find those 9 solvable problems, the agent had already run all 353 — burning money on every single one. The complete exploration cost is far higher than the per-problem success cost. The paper admits this in the main text, but readers should keep it in mind.

There's a gap between formalization and informal mathematics. Translating Erdős problems from natural language into Lean can itself introduce bias. Does "density" mean "lower density" or "natural density" — two problems in the paper were only solved after correcting this ambiguity. The agent found a proof for the "natural density" version, revealing that the human authors' formalization was imprecise. This is both a highlight and a hidden danger: how do you know the uncorrected problems don't harbor similar ambiguities?

What do the proofs look like? The agent's Lean proofs are machine-readable; only with the "deformalized" natural-language versions in the supplementary material can human mathematicians read them. But the "deformalization" step — translating Lean code back into human-readable proof — can itself introduce misunderstandings. The paper provides curated natural-language proofs, carefully reviewed. But no full peer review of all nine proofs was done.

Clear domain preference. What the agent excels at — combinatorics, number theory, optimization — happens to be where the Lean math library (mathlib) is most mature. Algebraic geometry stopped at codimension 3. Complex topology, representation theory, analytic number theory — the paper didn't touch them. This is a ceiling imposed by tool maturity, not by LLM capability.

---

🦾 Stepping Back: The Compiler as Mathematics' Lie Detector

The paper's most fundamental contribution is not "AI solved 9 Erdős problems." Those nine have their own value. What matters more is that it demonstrated the viability of a path —

Using formal verification to tame LLM uncertainty.

The mathematical community's greatest fear about AI is not "it will replace human mathematicians." It is "it will drown the human mathematical enterprise in arguments that look correct but are wrong." If every arXiv submission day brought hundreds of AI-generated "proofs" with logical holes, the peer review system would collapse.

Formal proofs — verified line by line by a compiler — are the natural barrier against this crisis. It places a lie detector between mathematics and AI. The LLM can talk big, fabricate lemmas, guiltily stamp sorry — but the compiler doesn't buy it. A "proof" that doesn't compile is void.

This paper made that idea work on open problems. Nine problems, all with complete, machine-verifiable Lean proofs. You don't need to trust DeepMind. You only need to trust the Lean compiler — and the Lean compiler is open source; anyone can verify it themselves.

This points toward a far grander picture. If formalized proofs become a standard format for mathematical publication — as ubiquitous as LaTeX is today — then AI and human mathematicians stand equal on this track. Human-written proofs must pass through the compiler too. AI-written proofs must pass through the compiler too. Who wrote it doesn't matter; what matters is whether the compiler's light is green or red.

There's a sentence in the paper, unremarkable, but the footnote to this whole piece:

> "Because the sketches were formal, experts could focus on the unresolved subgoals rather than re-verifying the entire argument."

The proofs are formal. Human experts don't need to re-verify from scratch — they only need to look at the part the agent couldn't crack. The time saved goes elsewhere.

This, perhaps, is more thought-provoking than the answers to those nine Erdős problems themselves.

---

💭 Coda: The Other Side of Money

One last thing.

A word keeps recurring in this paper — cost. Inference cost. Compute cost. Dollars per problem. The optimization target and evaluation metric are not accuracy, not pass@k — it's how much money it takes to solve a problem.

Having read dozens of AI papers, very few report "money" as a core metric. The usual move is to compare accuracy — "we're 2.3 percentage points above baseline" — put that number in a table with a little asterisk, and say nothing about the GPU hours, electricity, or dollars behind those two points.

This paper doesn't dodge. It puts Gemini 3.1 Pro's API pricing in the appendix, lists AlphaProof's TPU time and unit cost in the experiments section, and plots every cent of the gap between full and basic versions in cost–success-rate scatter charts. Average inference cost per problem, cost tables for 6 problems × 4 agent variants × multiple parallelism settings — all public.

This isn't just about transparency. It's about a principle: mathematics belongs to everyone. If an AI system can prove theorems but only Google can afford its bill — it isn't helping mathematics; it's helping the mathematics of the rich.

The paper notes that even the basic Agent A (LLM + compiler loop, no AlphaProof or evolutionary search) solved all nine problems. What does that mean? It means the cheapest version — a large-model API call plus the open-source Lean compiler running locally — can be replicated by any math graduate student with a few hundred dollars of budget.

This is a rare moment when "reproducibility" went from a slogan to a line item of dollar figures.

---

📚 References

1. Tsoukalas, G., Kovsharov, A., Shirobokov, S., et al. (2026). Advancing Mathematics Research with AI-Driven Formal Proof Search. *arXiv:2605.22763*. 2. Hubert, T., Schirrmacher, M., et al. (2025). AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems. *Nature*. 3. Novikov, A., Sener, O., et al. (2025). AlphaEvolve: Evolutionary Search for Scientific Discovery. *arXiv*. 4. de Moura, L., Kong, S., et al. (2015). The Lean Theorem Prover. *CADE-25*. 5. Feng, Y., et al. (2026). Aletheia: An AI Mathematician. *arXiv*.