AI system with no fine-tuning proves all 6 IMO 2026 problems in Lean

Researchers at Case Western Reserve University (the work was done during an internship at Amazon Web Services) have shown that an off-the-shelf large language model, with no fine-tuning at all, can prove hard theorems and program correctness if the work around it is organized well. They used Anthropic Fable-5 as the model. The proofs are written in Lean, a language in which a small "kernel" checks every reasoning step, and the kernel cannot be fooled.

The system solved all six formalized problems from the 2026 International Mathematical Olympiad. It also passed all VERINA tasks (a verified-programming set) and worked through the verification conditions from NTP4VC, an industrial formal code verification set. In addition, it solves problems from PutnamBench, a set of formalized problems from the Putnam university competition.

Every counted result is either a proof or a disproof of a statement, and the Lean kernel checks both.

An agent tree instead of a series of restarts

The difficulty is that Lean answers only a local question: does a given step go through? A bad decomposition of the problem, or a missing lemma (an auxiliary statement), shows up only dozens of steps later. On top of that, the model is limited by its context window and compute budget.

The authors solve this recursively. A main agent launches child agents, and each one looks for either a different proof strategy or a needed lemma. The details work like this:

• each child has its own clean context and its own copy of the project; • a child can spawn children of its own, and all agents use the same tools; • a child may spend dozens of calls on a single lemma, but returns to its parent only the finished lemma, a counterexample, or partial findings; • results reach the parent on its next turn, without waiting for the other branches, so an early finding can redirect the search; • the search ends when the first suitable proof is accepted.

In spirit this resembles Monte Carlo tree search, but the model itself makes the decisions. It reads the contents of its children's answers and decides which branches to continue, change, or expand. Visit counters and averaged value estimates are not used.

Another tool is parallel tactic probing. The agent launches several candidate tactics at once on the current proof state. The one that works goes back into the context, while traces of the failed attempts are discarded, so the context does not get cluttered.

Lean as a scalable service

The hardest proofs required dozens of subagents in a single run. A single machine did not have enough compute for Lean, so the team moved checking into a separate stateless service. Clients send Lean source code over JSON-RPC instead of referring to local files. Any ready replica with the same Lean and Mathlib versions can handle any request.

Inside each replica is a pool of worker processes with the Mathlib library preloaded. Importing takes tens of seconds, so the processes are reused, and checking on a "warm" process is noticeably faster. The replicas run in Kubernetes, and their number adjusts automatically to the load.

The system has separate protection against cheating. An agent editing a proof file could weaken the theorem statement, leave a sorry placeholder, or add an axiom. So everything up to the theorem signature is frozen, and the final check is done by Lean Comparator: the file must compile without placeholders and use only permitted axioms. The agent's own report of success is not taken into account.

A new exam: competition code as verification tasks

The old benchmarks are nearly exhausted, and hand-written code verification sets are small: they contain hundreds of tasks, which can be memorized or found in training data. So the authors built a pipeline that generates tasks automatically:

• a coder agent writes safe Rust solutions for LeetCode-style problems, where a single pure function operates on simple data (numbers, lists, strings, trees, linked lists); • the solution passes reference tests, then is translated into an executable model in Lean; • Rust and Lean are run on the same inputs, and only programs whose outputs match completely are accepted; • a separate agent writes a specification, that is, a property that must hold or fail; • the statement is frozen, and the prover either proves or disproves it.

What sets this apart from hand-written sets is that the tasks carry implementation-level obligations: fixed-width arithmetic, explicit errors, generated loops, type casts, and functional replacement of mutable state. Disproofs yield negative labels, which proof-only pipelines lack. A different agent writes the specification before the prover ever sees it, and the prover cannot choose an easier formulation.

On a sample of statements with a 30-minute limit for each, the system solves only some of them. For a prover that has nearly exhausted the old benchmarks, these tasks remain far from saturated. They can be scaled with compute, used to compare other provers, and used as rewards in reinforcement learning with verifiable rewards (RLVR). The code benchmark does not "guess" anything; it produces a verifiable verdict from the kernel. Program mutations (small edits to correct code) yield additional tasks with negative labels, but the paper does not evaluate them.

What this means for engineers

The main practical takeaway: without fine-tuning, the emphasis can go on the scaffolding. Context isolation, asynchronous search, parallel probing, and an elastic checking service let an ordinary model get a result out of Lean that previously required specially trained models such as Goedel-Code-Prover. Anyone building agents for code verification can also use the scheme of a frozen statement plus an independent final check: it closes off the typical ways of fooling the verifier.