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

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:

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.

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 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:

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".

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.

Two details in the design matter more than they look:

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.

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:

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.

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:

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.

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:

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.

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.

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:

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