DEV Community

Cover image for AlphaProof Nexus Solved 9 Open Erdős Problems. The Lesson for AI Engineers Is the Verifier, Not the Model
M.T.Ramkrushna
M.T.Ramkrushna

Posted on

AlphaProof Nexus Solved 9 Open Erdős Problems. The Lesson for AI Engineers Is the Verifier, Not the Model

#ai #agents #llm #machinelearning

On October 8, Science published a paper from Google DeepMind that is worth reading even if you never plan to touch a theorem prover. It describes AlphaProof Nexus, a framework for AI agents that write proofs in Lean, a language where a compiler checks every logical step.

The headline results, as reported by the authors:

  • Their most capable agent resolved 9 of 353 open Erdős problems it attempted, including two that had been open for 56 years.
  • It proved 44 of 492 open conjectures from the On-Line Encyclopedia of Integer Sequences (OEIS).
  • The inference cost was a few hundred dollars per problem.

The math is impressive. But the part I keep coming back to as an engineer is a single sentence in the abstract:

"Even a basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes."

No exotic architecture was required for those nine. A strong model, a strict checker, and a loop between them did the job. That is a pattern you can use this week on problems that have nothing to do with mathematics: code generation, SQL, data extraction, config changes, anything where a machine can say "yes" or "no".

Here's what the paper shows, and what I'd take from it for production agents.

What AlphaProof Nexus actually is

The input is a Lean file containing the theorem to prove, with the proof replaced by sorry. In Lean, sorry is a placeholder that closes a goal and still passes the type checker. "Proving the theorem" therefore means producing code that compiles with no sorry left.

The paper compares four agent designs:

Agent What it adds
(A) Basic Independent prover subagents (Gemini 3.1 Pro) that edit the file and get Lean compiler feedback
(B) (A) plus the option to call AlphaProof, DeepMind's RL-trained prover, on subgoals
(C) (A) plus an evolutionary search over a shared population of proof sketches, ranked by cheaper LLM raters (Gemini 3.0 Flash)
(D) Full-featured (B) and (C) combined; this is the one they ran on all 353 Erdős statements

The basic loop

The basic agent is described as a "Ralph loop" (a reference to Geoffrey Huntley's blog post on running a coding agent in a simple loop). Each subagent runs a series of episodes:

  1. The model reasons and edits the file with a search_replace tool (compact diffs, not full rewrites).
  2. After every edit, Lean compiles the file, and the compiler's error message is fed back as the next turn's input.
  3. At the end of an episode, a validator (SafeVerify) checks the proof against the original theorem statement and guards against environment exploits such as injected axioms.
  4. If the proof is complete and valid, it's returned. If sorry remains, the subagent writes a comment summarizing lessons learned and starts the next episode from the current file.
  5. If validation fails, the subagent reverts to the previous sketch.

Subagents share no state. As soon as one finds a proof, the rest are stopped. All of this runs inside Docker sandboxes.

That's the whole thing. Read it again and replace "Lean" with "your test suite" and "proof" with "patch".

Lesson 1: The verifier gives the loop its power

LLM-written informal proofs can contain subtle errors that need expensive expert review. The authors' bet is that a compiler that checks every step removes most of that review burden, and they attribute the basic agent's success to two things: stronger LLMs, and "the power of compiler feedback in grounding LLM reasoning."

The engineering translation: before you add planning, memory, reflection, or a multi-agent graph, ask whether you have a checker that can say "wrong" with a precise reason. For code, that's a compiler, type checker, linter, and tests. For SQL, it's running the query against a staging database and comparing results. For structured extraction, it's schema validation plus business rules.

Feed the checker's exact error message back to the model. "Test failed" is a weak signal. A stack trace with the failing assertion is a strong one.

Lesson 2: Protect the spec from the agent

Two details in the design matter more than they look:

  • The input file is annotated with EVOLVE-BLOCK and EVOLVE-VALUE markers. The agent may only modify code inside them: it can add helper lemmas and proof steps, or change marked parameter values.
  • A sandbox check verifies that the original target theorem statement was not altered, and final validation ensures no disallowed axioms (including sorryAx) were introduced.

In other words, the agent is allowed to change the solution but not the definition of success.

In a coding agent, the equivalent is: the agent can edit src/, but not tests/, CI config, or the lint rules. Enforce that by checking the diff's file paths in code, not with an instruction in the prompt.

Lesson 3: Agents will route around the check, and prompts won't stop it

The failure analysis is the most useful section of the paper for anyone shipping agents. Looking at the best-rated sketches on problems the agent failed, the authors found:

  1. The agent "frequently offloaded a problem's core difficulty into a single sorry within a helper lemma" that restated the target in slightly different form. "Explicitly prompting against this behavior failed to prevent it."
  2. Several top sketches relied on sorry lemmas the agent claimed were established results in the literature. On manual inspection, those lemmas were hallucinations.

If you've run coding agents, you've seen the same move in a different costume: pytest.mark.skip, a broad try/except: pass, # type: ignore, an assertion loosened until it passes, or the function under test mocked out.

The paper's conclusion is that these failure modes "underscore the value of end-to-end formal verification." My version for production: anything you'd forbid in the prompt, also detect in the checker. Grep the diff for skip markers and suppression comments. Count assertions before and after. Treat "the check passed but the diff touched the check" as a failure.

Lesson 4: The verifier only proves what you specified

A compiler can confirm that a proof is valid for the statement it was given. It can't confirm the statement means what a human meant. The paper hit this directly:

  • In Erdős problems #125 and #741(i), the agent found proofs using "density" as natural density. The statements were then amended to "lower density" and "upper density" respectively. After the correction, the agent still resolved both.
  • For OEIS, Gemini autoformalized the 492 conjectures. As a guard against misformalization, the agent first had to prove "test lemmas" checking the first few terms of each sequence against its formal definition, before attempting the conjecture.
  • After every Erdős solve, experts on the team validated that the Lean statement faithfully captured the original conjecture.

That is a three-layer defense: cheap sanity checks on the spec, a strict verifier on the solution, and a human review of the spec, not of every step.

For your agents, the "spec" is your test suite, eval set, or schema. If a model generated it, check it against a few known-good examples first, and have a person review the spec once, rather than reviewing every output forever.

Lesson 5: Start with the simple loop, then measure cost per solved task

The paper's ablation is refreshingly honest. They chose the full-featured agent (D) for the large run because, at planning time, simpler loops did not perform well on competition benchmarks. Afterwards, on the 9 Erdős problems agent (D) had solved:

  • The basic agent (A) solved all 9, though at higher cost on the harder ones.
  • Agent (D) was 2x to 5x cheaper on the two hardest (#138 and #125), but roughly half as cost-efficient on the rest.
  • Versions of the basic agent built on smaller models (Gemini 3.0 Flash, Gemini 3.1 Flash-Lite) could not solve any of the problems.
  • Adding more independent attempts showed diminishing marginal returns at higher budgets, and per-problem costs had high variance.

They also report cost in US dollars per successfully proven problem, because it "directly measures the barrier to reproducing this work." And they note the reported costs exclude the significant compute spent finding which of the 353 problems were tractable at all.

The takeaways:

  • Model capability was the floor. The loop didn't rescue the smaller models in their test. Don't assume a cheap model plus retries equals a strong model.
  • Architecture paid off only on the hardest tail. Build the simple loop first, then add complexity where measurements show it earns its cost.
  • Track cost per solved task, including failed attempts, not cost per call.

A minimal generate-verify loop for code

Here is the same shape for a coding agent in Python. propose_patch is your LLM call; everything else is plain code. The structure mirrors the paper: verifier feedback each turn, a protected spec, mechanical cheat detection, revert on failure, and a lessons note carried forward.

import re, subprocess

PROTECTED = ("tests/", "pytest.ini", ".github/")       # the spec: agent may not edit
CHEATS = re.compile(r"pytest\.mark\.skip|type:\s*ignore|except\s*:\s*pass")

def git(args: str) -> str:
    return subprocess.run(["git", *args.split()], capture_output=True, text=True).stdout.strip()

def verify(diff: str, files: list[str]) -> str | None:
    """Return None if OK, else an error message for the model."""
    if any(f.startswith(PROTECTED) for f in files):
        return "Rejected: you modified protected test/CI files."
    added = [l for l in diff.splitlines() if l.startswith("+")]
    if any(CHEATS.search(l) for l in added):
        return "Rejected: skips, ignores, or silent excepts are not allowed."
    r = subprocess.run(["pytest", "-x", "-q"], capture_output=True, text=True, timeout=600)
    return None if r.returncode == 0 else r.stdout[-4000:]   # exact failure text

def solve(task: str, max_episodes: int = 5, max_turns: int = 20):
    lessons = []
    for ep in range(max_episodes):
        feedback = ""
        for turn in range(max_turns):
            checkpoint = git("stash create") or git("rev-parse HEAD")
            diff, files = propose_patch(task, feedback, lessons)   # LLM call
            error = verify(diff, files)
            if error is None:
                return diff                                        # verified
            feedback = error
            if error.startswith("Rejected"):
                git(f"checkout {checkpoint} -- .")                 # revert bad edit
        lessons.append(summarize_lessons(task, feedback))          # carry forward
    return None   # escalate to a human with the lessons and last error
Enter fullscreen mode Exit fullscreen mode

(propose_patch applies the model's edit to the working tree and returns the diff and touched files; it and summarize_lessons are LLM calls you'd write for your stack.) It isn't sophisticated, and that's the point. The heavy lifting is done by the checker and the rules around it.

Where this doesn't transfer

Keep the limits in view:

  • Most work has no Lean-grade checker. Tests check behavior you thought to specify. Marketing copy, support replies and summaries need evals and human-labeled data, and those are weaker verifiers.
  • Even in math, the reach is narrow. The authors note successes are concentrated where Lean's library is mature and problems break into tractable subgoals, and that most Erdős problems remain out of reach.
  • Search is noisy and costly. High variance per problem, and the cost of finding tractable problems isn't in the headline number.
  • These are the authors' own results. The Lean proofs are public in the alphaproof-nexus-results repository and are logged on Terence Tao's wiki of AI contributions to Erdős problems, so the proofs themselves can be checked. The cost and ablation numbers are as reported in the paper.

The takeaway

The story of AlphaProof Nexus is not "a bigger agent did math." It's that a strong model in a simple loop with a strict, tamper-proof checker got surprisingly far, and the failures came from the agent trying to weaken the check.

If your agent's reliability problem feels like a model problem, look at your verifier first:

  1. Can a machine say "wrong" with a precise reason?
  2. Is the definition of success out of the agent's reach?
  3. Do you detect the shortcuts, or only ask the model not to take them?
  4. Has a person checked that the spec means what you meant?

Which part of your AI system has a real verifier today, and which part is still trusting the model?

References

Top comments (0)