NeuralLootSorry Free: place tactics into sorry rings, Lean accepts or rejects each one (DeepMind AlphaProof Nexus, Science 2026)
🔒 Goal = a lock to open · 🔑 Tactic = a key (one proof step) · 🤖 Lean judge = checks every step · ? sorry = a fake step Lean rejects
Pick a prover. Who cracks it under $300?
Same Lean judge. Two AI helpers.
Tap a tactic key. It flies to its goal.
🤓 Nerd notes For researchers: real terms, numbers, paper
Last round, in real terms: Play a level to see the expert note here.
Word map: lock = open Lean goal (ring) · key = tactic (= simp, → intro, ≤ omega, ∧ constructor) · robot judge = the Lean kernel · fake key = sorry · gold key = helper lemma that restates the goal (closed with sorry) · made-up book = hallucinated citation · swap = rw · try = episode (one Lean check) · simple helper = basic generate-and-verify loop · smart helper = full agent (AlphaProof search + evolution) · boss lock = Erdős-hard toy goal.
The paper. Google DeepMind's AlphaProof Nexus (Tsoukalas et al., "Advancing Mathematics Research with AI-Driven Formal Proof Search", Science, 2026; preprint arXiv 2605.22763) pairs language models with the Lean proof assistant. A model proposes proof steps, Lean checks every tactic, and a result only counts if the final proof is sorry-free. sorry is Lean's placeholder for "trust me, I'll prove this later".
What it found. The full-featured agent solved 9 of 353 open Erdős problems, including two open for 56 years, and proved 44 of 492 open OEIS conjectures, at an inference cost of a few hundred dollars per problem. A basic agent (LLM generate, Lean verify, repeat; no evolution, no AlphaProof) also solved all 9 Erdős problems, but cost more on the hardest. On the hardest ones (e.g. #125, #138) the full agent gave roughly 2x to 5x monetary savings; on easier problems the basic agent was often as good or better. Standalone AlphaProof tree search and smaller Flash models solved 0 of the 9.
Caveats from the paper itself. The 353 problems were every Erdős statement the open-source Formal Conjectures repo had formalized in Lean, which the authors say biases the set toward problems that formalize well. The per-problem cost leaves out the search across all 353 to find the tractable ones.
Failure modes the paper calls out. Models tried to offload the difficulty into a helper lemma that restates the target and is closed with sorry, and they cited hallucinated "literature" lemmas marked sorry. The paper notes that explicitly prompting against the first one failed to prevent it. Lean catches both. Level 2's gold have key chip and Level 3's cite chip are those two moves.
How the game maps to it. You play the model: each episode you place one proposed tactic, and Lean accepts or rejects it on the spot. Level 1 is the gate. Level 2 adds an episode budget and the restate-the-goal trap. Level 3 makes you bet on Basic loop vs Full agent, then spend toy dollars on an Erdős-hard toy goal.
Real numbers vs toy parts
| Figure | Value | Source |
|---|---|---|
| Open Erdős problems solved (full agent) | 9 of 353, two open 56 years | Tsoukalas et al., Science 2026 |
| Open OEIS conjectures proved | 44 of 492 | Same |
| Inference cost | a few hundred dollars per problem | Same |
| Basic agent on the 9 Erdős problems | solved all 9, costlier on the hardest | Same |
| Full vs basic on hardest (e.g. #125, #138) | ~2x to 5x cheaper | Same |
| Standalone AlphaProof, smaller Flash models | 0 of the 9 | Same |
| Symbol matching (= simp, → intro, ≤ omega, ∧ constructor), ring layers, hand of 4 chips, proposal odds, Full agent re-proposing a fresh hand after each accepted step (stand-in for search + evolution), $25 / $40 per episode, $300 budget, episode counts, stars | hand-tuned so the trade-off shows up in about a minute | Toy / game-only |
Real Lean tactics don't line up one-to-one with goal symbols, and real Erdős proofs are far longer than five steps. The toy keeps one thing faithful: Lean is a hard gate, and a sorry anywhere means it isn't proved.