Storing verified lemmas instead of context gets an agent to olympiad gold

Over the past couple of years, large reasoning models (LRMs) have gotten noticeably better at olympiad math. On problems at the level of AIME (the American Invitational Mathematics Examination), one long reasoning pass is usually enough: the model writes out a chain of thought, checks the answer, sometimes takes a couple of runs at it — and lands it. IMO (the International Mathematical Olympiad) is hard in a different way. A solution there rarely fits a single straight line: you have to try ideas, back out of them, write down the intermediate facts you've established, and then build the proof out of those bricks. And this is where models run into a fairly mundane wall — the context limit. Even 64k or 128k tokens turn out to be cramped for some proofs, once the reasoning sprawls and the intermediate findings get buried in the noise of the draft.

The authors of Long-horizon Reasoning Agent for Olympiad-Level Mathematical Problem Solving suggest framing the task differently: don't try to cram the whole solution into one pass, build an agent that can work for a long time, in stages, the way a person does.

The idea: reason iteratively, and work in lemmas rather than text

The Intern-S1-MO agent works in rounds. In any given round it isn't required to finish the problem off. The round's key artifact is something else: carefully stated intermediate results — lemmas, useful observations, partial proofs. Those can then be reused.

To make that work, the system is built as three agents with three roles. The first tries to solve the problem and explore ideas. The second compresses the resulting draft into a compact set of lemmas — no repetition, no dead-end branches, no surplus reasoning. The third checks the lemmas so that errors don't leak into memory: one wrong lemma can drag a whole chain of false conclusions behind it and burn the entire attempt budget.

So the system's memory isn't a giant reasoning log but a structured library of lemmas. The format is a human one: we also try to hold on not to every trial attempt but to what has actually been proved and will be useful later.

Keeping the lemmas honest

The paper puts a lot of weight on verification. Lemmas are checked by several independent runs of the verifier agent, and the resulting confidence is aggregated — which lowers the risk that a convincing-sounding statement slips through as truth by luck. The final proof gets a separate check: a dedicated process verifier looks for logical holes step by step and returns written feedback, after which the solution can be fixed iteratively.

In practice this closes off a familiar LRM failure: when the budget runs out, the model often commits to a premature answer. Here it has a safe mode instead — bank the progress as lemmas, even if there is no complete solution yet.

Training for long horizons

Architecture on its own is no guarantee that the model will actually learn to carry out long iterative reasoning. So the authors add an RL framework, OREAL-H, that fits training to the hierarchical process: there are high-level actions (switching to lemma extraction or to verification, for instance), there is text generation, there are intermediate signals from the verifier, and there is the final reward for a correct answer.

A lemma dependency graph hands out credit to the intermediate statements that genuinely led to a successful solution. It amounts to an attempt to reward honestly — not just the final answer, but the reasoning stages that made that answer possible.

What the benchmarks and a live competition showed

Across the experiments, the system posts strong numbers on several kinds of problems. On AIME2025 and HMMT2025 the reported figures are 96.6% and 95% pass@1. On the non-geometry problems of IMO2025 it scores 26/35, on par with a silver medalist. On CNMO2025 it gets 232.4/260 (again without geometry). And the most telling result is its entry in CMO2025, where expert graders put the agent at 102/126 — comfortably above the gold threshold.

From a practical standpoint, what matters here isn't only the score but the demonstration of the mechanism: the system can spend a large inference budget sensibly instead of turning it into an endless stream of tokens. The authors state the scale outright, on the order of 512K tokens per problem, but stress that the key is not a bigger context — it's how you store and reuse the progress you've made.

Why it matters

The work draws a clear line between solving a problem in one burst and solving it as a series of deliberate steps that can be checked and saved. At olympiad level, the second is what counts. The lemma approach looks like a middle ground between purely textual reasoning and heavyweight formal proof: it keeps the convenience of natural language while still making memory manageable and errors catchable.

The limits are legible between the lines too. First, a heavy dependence on verifier quality: if the checking fails systematically, memory will start accumulating garbage. Second, the authors explicitly exclude geometry from several of the evaluations — it remains a hard case. But as an architectural idea for long-horizon reasoning, this looks like a convincing step forward.