A language model answers a competition problem in thirty seconds, while another system is handed a theorem and works on it for a day, sometimes returning a proof. These look like the same activity run at two budgets, and the natural extrapolation is that a day is simply a longer chain of thought: sample for longer, sample more often, train the policy harder. That reading is a fair summary of the public literature, and it is where most of us start.
It breaks for two reasons, both of which concern what a single trajectory cannot do. A chain of thought retains nothing once its context ends; and two half-finished chains of thought cannot be combined into one. Everything in this design space is a response to those two deficits.
What follows is an attempt to put the current crop of systems into a single frame. I will not describe any optimiser, any architecture variant, or any of the policy-gradient bookkeeping, since that material is well covered elsewhere and is not where the interesting differences live. Those differences are about where truth is cheap, where it is unavailable, and what survives between contexts.
From pretraining to a deployed assistant
The systems below sit on top of the standard pipeline rather than replacing it, so this section fixes vocabulary rather than explaining anything. The first stage needs no introduction at all.
Pretraining fits a model to predict the next token over an enormous corpus, and what comes out is a distribution over continuations. Nothing in that objective asks for a system that answers a question, follows an instruction, or stops when it is done. The remaining stages exist to supply those.
Supervised finetuning supplies them. Collect demonstrations of the behaviour you want, prompts paired with good responses, and continue training on those. A continuation engine thereby becomes something that behaves like an assistant, and this stage is cheap, stable, and limited by how many demonstrations you are willing to write.
Preference tuning handles what demonstrations cannot. For questions of helpfulness, tone, verbosity or refusal there is often no single correct response, but people can reliably say which of two responses they prefer. So collect comparisons, fit a reward model to them, and use reinforcement learning to push the policy toward responses the reward model scores highly (Ouyang et al. 2022). This is the stage usually meant by RLHF, and it is what turns a competent model into one people are willing to use.
Those three stages have been the standard recipe for several years, and they produce the assistants everyone is familiar with. The reasoning models are what you get when a fourth stage is added: more reinforcement learning, on problems whose answers can be checked automatically, at very large scale. That stage is the subject of the next section and the foundation of everything after it.
Two observations before moving on. First, these stages compose rather than compete; a reasoning model has typically been through all four, and a deployed product then wraps the result in further scaffolding, such as system prompts, tool access and sampling settings. Second, and more important for what follows, every one of these stages produces the same kind of object. A policy. Given a prompt it returns a distribution over responses. Everything in the rest of this post concerns what one builds around such a policy once the questions get hard enough that a single response will not do.
The workhorse: where the reward comes from
That fourth stage is a variation on the loop we just met, so here it is in one paragraph. Anyone who has done preference tuning will recognise the machinery, because the machinery is the same. What changes, and what the whole post turns on, is where the reward comes from.
Take a prompt \(x\). Sample a group of \(G\) completions from the current policy,
\[ y_1, \ldots, y_G \;\sim\; \pi_\theta(\cdot \mid x), \]
score each one to get a reward \(r_i\), then increase the probability of the completions that scored well relative to the others in their own group, and repeat. The only structural novelty worth mentioning is that the baseline comes from the group itself: with \(G\) samples of the same prompt, the mean reward within the group estimates how hard that prompt is, so no separate value network is needed. This is what GRPO (Shao et al. 2024) does, and the details beyond it are bookkeeping I will not dwell on.
Everything interesting sits in the scoring step, and the options form a spectrum rather than a single choice.
At one end the reward is a program. A competition problem with a short answer can be scored by extracting the boxed expression and comparing it to a reference; a coding task can be scored by compiling the program and running its tests. The reward is then a bit, produced by code, and this is the case that acquired the name reinforcement learning with verifiable rewards.
In the middle sits a learned preference model, trained on human comparisons. That is ordinary preference tuning, it long predates the reasoning era, and it remains what one uses for helpfulness, tone and safety, where no program can settle the question.
Further along, the scorer is another language model reading the output against a written rubric. This is how one attacks domains that have no checker but do have criteria, such as medical advice or open-ended writing (Gunjal et al. 2025), and we will meet it again in an unexpected place: a formal theorem prover whose most important component is supervised this way, because the kernel has nothing to say about the thing being judged.
At the far end the reward is a vote, with a model’s own agreement across samples standing in for a label it does not have.
Only the first of these is safe under heavy optimisation, and that is the whole reason the program end matters. A learned scorer can be fooled, so pushing hard against one finds the places where it is wrong rather than the places where it is right. A unit test cannot be flattered, and neither can an arithmetic check. Since the reward is code, running a policy against it a hundred million times is safe in a way that running against a critic is not.
Two clarifications, since both matter later.
First, verifiable does not mean mathematical. The territory is large and commercially important: code against test suites, SQL that either returns the right rows or does not, formatting and instruction-following constraints that can be checked syntactically, tool calls that either parse or fail. This loop is the workhorse behind most of what the last two years called reasoning, and within its territory it is genuinely general.
Second, the checker is a training-time object. It needs the reference answer, so it exists while you are building the model and is gone the moment a user asks a real question. At deployment the policy generates and nothing checks it. That distinction explains a great deal of what follows, including why a system can be demonstrably capable of producing a correct answer and still fail to give you one.
Now notice what the program end of the spectrum requires: a finished artifact the code can run, and a reference to compare it against. A proof has neither, since there is no reference string, and checking it means checking an argument rather than an output. The rest of this post is about that boundary, and the first thing to observe is that the field’s flagship result ran straight into it and said so.
Two facts that break the naive picture
DeepSeek-R1 (Guo et al. 2025) is the paper that defined the field’s current phase, and it showed that reinforcement learning against a verified final answer produces long chains of thought, with backtracking and self-checking emerging without ever being specified. Buried in its supplementary material, however, is one sentence that should stop anyone reading it with proofs in mind:
Mathematical proofs are excluded because it is difficult to determine their correctness.
The training set is competition problems with short checkable answers, and proofs were left out because correctness could not be established. The capability boundary and the verifier boundary are therefore the same boundary, and the most celebrated result in reasoning RL defines the task we care about here as out of scope.
The second fact concerns the other obvious move, which is to sample more. Brown and coauthors (Brown et al. 2024) measured what repeated sampling actually buys. Solving MATH problems with Llama-3-8B-Instruct, they report, “coverage increases from 82.9% with 100 samples to 98.44% with 10,000 samples”. Yet “when using majority voting or reward models to select final answers, the biggest performance increase is only from 40.50% to 41.41% over the same sample range”. Two orders of magnitude of inference compute therefore bought nine tenths of a point, and every selection method they tried, majority voting included, plateaus before a hundred samples.
Put together, these foreclose both easy roads. Thinking longer runs into a verifier that cannot check what you produced, and sampling more runs into a selector that cannot tell you which sample was right. Whatever these systems are doing, then, it is something else, and naming it requires first naming the parts.
The parts
There are six objects, and every system below is a choice of the six.
A goal \(g \in \mathcal{G}\) is a statement to establish or a question to answer, and a policy \(\pi_\theta(a \mid g, c)\) generates an artifact \(a\) for that goal in some context \(c\). A hard verifier \(V(g,a) \in {\left\{ 0,1,\bot \right\}} \) is the trusted oracle, where \(\bot\) means that the oracle has nothing to say rather than that the artifact is wrong; that third value is the subject of most of this post. Against it sits a soft evaluator \(\widetilde{V}(g,a) \in [0,1]\), which is anything that scores without being trusted: a learned value function, a neural judge, a vote. Finally, a persistent store \(\Sigma\) is whatever survives when a context window ends, and an allocation \(\mathsf{A}\) distributes a compute budget over goals and over time.
One operator does more work than the rest. A decomposition
\[ D : \mathcal{G} \longrightarrow \mathcal{G}^{k}, \qquad g \longmapsto (g_1, \ldots, g_k) \tag{1}\]
turns one goal into several, and it comes with an obligation that does the real work: a proof of \(g\) conditional on \(g_1, \ldots, g_k\). Without that obligation, a decomposition is merely a list of wishes.
A system is then the tuple
\[ \mathcal{M} \;=\; {\left( \pi_\theta, \; V, \; \widetilde{V}, \; D, \; \Sigma, \; \mathsf{A} \right)} , \tag{2}\]
and the claim I want to make is that the differences between the systems in this literature are choices of slots rather than differences of scale.
Where verification stops
The hard verifier \(V\) is defined on finished artifacts and on nothing else. Call that boundary the verification frontier. Below it, truth is free; above it, we are guessing.
Where the frontier sits depends on what we are willing to accept as an artifact. For a Lean proof it sits at a complete proof term, and the kernel’s verdict is about as close to absolute as anything in this business gets. For a final-answer matcher it sits at the boxed answer, so everything above it, meaning the entire reasoning trace, goes unchecked. For code it sits at a program that runs against tests.
Now consider a system that decomposes a hard theorem into lemmas, writing a proof sketch in Lean with the lemmas stated and their proofs left as sorry. That sketch compiles. A file full of sorry is perfectly valid Lean, so \(V(g, \text{sketch}) = 1\), and the verdict carries no information whatsoever.
The decision that matters most in a long run is how to break the problem apart, and it is precisely the decision that no oracle can score. Perfect verification at the leaves, in short, buys no verification of the plan. Since this holds in the one domain that has a genuinely trustworthy verifier, it is interesting rather than merely inconvenient.
Every system therefore needs a soft evaluator at its weakest point, whether or not its designers wanted one, and \(\widetilde{V}\) is always neural, always gameable, and always the component you would least like to depend on.
This casts the field’s retreat from process reward models in a rather different light. R1 removed neural reward models from its reasoning loop and said exactly why. The authors “abstain from applying neural reward models, whether outcome-based or process-based, to reasoning tasks”, because such models “are susceptible to reward hacking during large-scale reinforcement learning”. What replaced them was an answer matcher and a compiler, both of which sit firmly below the frontier. Read through the frontier, this was not a discovery that dense intermediate signal is unnecessary. It was a retreat from the region where signal cannot be trusted into the region where it can, and the price was paid in scope. The proofs went out of the training set in the same move.
Certification and selection are different jobs
While the frontier tells us that plans cannot be verified, it does not yet explain why anything works at all, and for that we need to separate two questions that look alike.
Certification asks whether a candidate \(a\) is correct, whereas selection asks which of \(a_1, \ldots, a_k\) to return. Certification demands an absolute judgement and its errors are unbounded in consequence, since a wrong accept ships a false result and nothing downstream is obliged to catch it. Selection demands only an ordering, so a badly calibrated scorer costs nothing provided its ranking survives the miscalibration; the scores are discarded the moment we take the argmax. Certification can also be supplied from outside, by a referee or a kernel at the end of the run, while selection cannot be outsourced at all, because it has to happen while the candidates are still in hand.
These two jobs have different difficulty, and the gap between them is measurable.
Recent work on generative verifiers (Mahdavi et al. 2025) trains a model to write out a verification rationale and emit a verdict, then uses that verdict to rank sampled proofs. At selection the approach works well: on a hard problem set, pass@1 moves from \(47.07\) to \(96.05\) with no hard verifier anywhere in the loop. Two caveats belong in the same breath as that number, though. The set is nineteen problems with integer final answers, chosen so the generator solves some but fewer than seventy percent of them. A single problem is therefore worth more than five points, and the baseline is partly a selection artefact. The lift also costs roughly a thousand model calls per problem, about half of them spent judging rather than generating. Selection at this quality is an inference system in its own right, not a post-process bolted onto the generator.
Point the same machinery at certification, however, and it stalls. Reinforcement learning on the verifier nearly doubles proof-level \(F_1\), yet final-answer precision moves only from \(60.41\) to \(62.59\), a difference the authors themselves describe as lying within the standard deviation. Worse, that flat precision is bought at collapsing recall, which falls from \(67.43\) to \(17.18\); the trained judge became far more willing to reject, and no better at telling right from wrong when it did accept. Reading these together tells us what the training actually did. The judge got better at producing verdicts shaped like a grader’s verdicts, and no better at deciding whether the mathematics holds.
The decisive experiment in that paper is small and brutal. Taking forty-eight olympiad-level proofs, every one of which contained a critical error, the authors asked a strong general model to grade them, and it accepted seven. The paper reports \(41/48 = 87.2\%\), which goes wrong twice over. First, the arithmetic is wrong, since \(41/48\) is \(85.4\%\) while \(41/47\) is \(87.23\%\), so a wrong denominator made it into the headline. Set that aside, though, because the honest number is the worse problem: on a set where every candidate is flawed, the constant policy “always reject” scores \(100\%\). A certifier at \(85.4\%\) is not nearly perfect; it is below trivial.
Given how much turns on the distance between the two jobs, it deserves a name. Write
\[ c(k) \;=\; \mathbb{P} {\left[ \exists \, i \leq k \, : \, V(g,a_i) = 1 \right]} \]
for the coverage, meaning the probability that \(k\) independent samples contain at least one correct answer, and write \(s(k)\) for the selection yield, the accuracy we actually obtain when \(\widetilde{V}\) alone decides what to return. Their difference
\[ \Gamma(k) \;=\; c(k) - s(k) \tag{3}\]
is exactly what we lose by not having a hard verifier at deployment. The numbers above give \(\Gamma(10^4) \approx 57\) percentage points on MATH, and the gap is not closing as \(k\) grows. Brown and coauthors put it well when they gloss coverage as performance with a perfect verifier; \(\Gamma\) is the price of not having one.
Which job a system needs, finally, decides what it is allowed to look like. If certification arrives from outside at the end, a system needs only a ranker, and rankers are what neural judges turn out to be good at. If certification has to be internal, the system needs a kernel, and it inherits everything that comes with formalisation. That is a genuine fork in the design space, and where a system sits on it explains more about its architecture than anything else we could ask.
What survives a context window
Both previous sections concern signal at a single instant, but a day is a great many instants, which raises the question of what is carried between them.
There are four rungs, and they map almost exactly onto timescales.
| \(\Sigma\) | Horizon | What it costs |
|---|---|---|
| nothing, independent samples | seconds | progress is never additive |
| the context window | minutes | dies when the window does |
| a file, a lemma library | hours | needs \(V\) to stay honest |
| the weights | days | needs training per problem |
The thesis of this post, in one line, is that compute compounds only where verification makes state durable.
A context window cannot compound, since nothing in it is checked before it is discarded. A lemma library compounds because a kernel-checked lemma is permanently true and permanently reusable. Weights compound whether or not the update was a good idea, which is both the appeal and the danger.
The property doing the work at the third rung is composability, and prose does not have it. Two partial chains of thought cannot be merged into one, whereas two proved lemmas can. Seed-Prover (L. Chen et al. 2025) makes this mechanical, promoting have blocks inside a proof to top-level lemma declarations. One bit per attempt thereby becomes a vector of bits over a decomposition, and in the authors’ words such lemmas “serve as shared knowledge” across separate attempts. Partial results thereby become addressable, storable, and mergeable across trajectories that never saw each other. A kernel, then, buys more than trust: it buys the ability to add.
One consequence falls out before we meet any systems. The horizon of a system is set by \(\Sigma\) and not by the quality of its policy. A frontier model with nothing but a context window still stops at the context window, while a weaker model with a file runs for hours. We will even see a case where nothing is trained at all and the system still closes open problems, which is difficult to explain on any account where capability lives in the weights alone.
Five ways to live with one bit
With the slots in hand, the literature sorts itself into five families, each an answer to the same question: what do you do when the only trustworthy signal arrives once, at the very end?
| Family | \(D\) | \(\Sigma\) | \(\widetilde{V}\) | Horizon |
|---|---|---|---|---|
| trajectory as search | identity | context | none, by choice | minutes |
| sample and select | identity | none | vote, reward model | seconds |
| decompose against a kernel | lemmas | lemma library | judge on sketches | hours |
| environment as memory | file edits | a file | subagent rating | hours |
| move the weights | identity | the weights | majority vote | a benchmark |
One caveat before we walk the rows. No two systems in this table were evaluated at matched compute on a shared benchmark, so the comparisons are unnormalised by construction, and we will come back to what that does to the field’s claims.
The trajectory carries the search
The first family bets that a long enough trajectory can implement search internally. There is no decomposition, the store is the context window, and the soft evaluator is deliberately absent, so backtracking and switching strategy become token patterns rather than components. R1, Kimi k1.5 (Team et al. 2025) and s1 (Muennighoff et al. 2025) all live here.
The mechanism is short, which is much of its appeal: sample, check the final answer, increase the probability of whatever worked. No value network, no process model, nothing scoring intermediate steps. Its boundary is the one we met above, since everything the family can do is downstream of what a matcher can check, and proofs are not.
Kimi makes the strongest version of the family’s claim, arguing that sufficiently long contexts allow planning and correction without tree search, value functions, or process rewards. It is a real position and may well be right, but it is never tested. The paper does have an ablation section, which covers model size, context length, the use of negative gradients, and sampling strategies; it does not ablate any of the three techniques it dismisses. What the paper establishes is that strong performance is reachable without them, and their own phrasing is careful about this, saying performance “can be achieved without relying on” the three. Whether any of them would have helped is a question nobody asked. Proof-style problems are also excluded from the prompt set by construction, so the family is never evaluated on the task this post is about.
The sharpest detail sits in their benchmark appendix. Kimi’s strongest single number is a Codeforces percentile, obtained, in their words, by “majority voting on the code snippets generated by the k1.5 long-CoT model, employing test cases that are also generated by the same model”. That is search over candidates with a soft evaluator, in the paper arguing that candidates need no search.
R1’s emergent-length curve deserves a note of a different kind. The paper reports that outputs were capped at 32,768 tokens before training step 8.2k and 65,536 afterwards. It then observes that “as a result, both the performance and response length of DeepSeek-R1-Zero exhibit a significant jump” at that point. The confound, in other words, is disclosed plainly by the authors; it is the retelling that drops it, and the retelling is where most of us met the result. The lengthening is real and the emergence story may well survive it, but a ceiling that moves at the same moment as the quantity it bounds weakens the curve as evidence.
The tempting reading of this family is that long reasoning is mostly cheap data plus a decoding trick, and s1 is usually cited for it. A thousand carefully chosen examples, a supervised finetune, and a crude intervention that forces the model to keep thinking by appending the token “Wait”. Their own appendix does not support that reading. Holding the same thousand questions, the same selection pipeline and the same training recipe fixed, and swapping only the teacher that generated the traces, AIME 2025 moves from \(26.7\) to \(50.0\). That swing is larger than the selection pipeline, worth \(13.3\) points over a random baseline, and budget forcing, worth \(6.7\), put together. Budget forcing then stops working altogether, since the improved model scores \(56.7\) and \(50.0\) on the two AIME sets identically at zero, one and two insertions of “Wait”. The ceiling, it turns out, is the teacher, and the teacher was trained with reinforcement learning.
Where the family stops is structural. Nothing survives the context and nothing is checked before it is discarded, so progress is never additive; the horizon is a context window, and no amount of model quality changes that.
Many attempts, then a choice
If one trajectory cannot carry the search, the obvious move is many trajectories. Here the store is nothing at all, every attempt starts from scratch, and the run is embarrassingly parallel, so the whole family is governed by \(\Gamma(k)\) from Equation 3.
We have already seen the shape of the problem, since coverage climbs while selection does not. Two further facts sharpen it.
First, coverage has a floor that sampling does not lift. In the same experiments, all eight Pythia models score zero coverage on CodeContests even at ten thousand samples; zero, not small. Sampling multiplies a nonzero probability, after all, and it cannot create one.
Second, allocation is a genuine design variable, and the compute-optimal result is usually remembered backwards. Snell and coauthors (Snell et al. 2024) asked when test-time compute beats simply training a larger model. To match the FLOPs of a model with \(M\) times more parameters, we may multiply the small model’s inference compute by
\[ M + 3 \, {\left( \frac{D_{\text{pretrain}}}{D_{\text{inference}}} \right)} \, (M-1), \tag{4}\]
where the ratio that matters is \(R = D_{\text{inference}} / D_{\text{pretrain}}\). Taking \(M \approx 14\) and \(R \in {\left\{ 0.16, \, 0.79, \, 22 \right\}} \), equation Equation 4 allows roughly \(258\), \(63\) and \(16\) generations respectively. Their conclusion is stated plainly: “on the harder questions or in settings with a higher inference load (\(R \gg 1\)), pretraining is a more effective way to improve performance”. A heavy inference load therefore favours the bigger model, because the pretraining surcharge amortises over all those queries. Test-time compute wins when \(R \lesssim 1\), which is the self-improvement and synthetic-data regime rather than the serving regime, and that is close to the reverse of the usual pitch about small models with clever inference.
Two caveats keep the result honest, and both cut toward the pretraining side being understated. The larger-model baseline is greedy pass@1, with no verifier and no sampling of its own. And the difficulty estimate that makes their allocation optimal costs 2048 samples per question, against allocated budgets of 4 to 256 generations. The router is therefore between eight and five hundred times more expensive than the thing it routes. That cost is excluded from the analysis; an appendix notes it “would be problematic” in production, which is fair but easy to miss.
Generative verification, from Section 6, narrows \(\Gamma\) for selection and not for certification, and that is the design consequence for this family. It can be made to work when something downstream supplies certification, and it cannot when it must certify itself. The family converts compute into coverage efficiently and into accuracy poorly, with the exchange rate set entirely by the quality of \(\widetilde{V}\).
Decomposing against a kernel
Both families so far treat the goal as atomic. The third breaks it, and this is where an hour becomes possible, because the durable unit stops being a token and becomes a checked lemma. The DeepSeek-Prover-V2 (Ren et al. 2025) line, the Seed-Prover line, and Aristotle (Achim et al. 2025) all belong here.
Seed-Prover 1.5 (J. Chen et al. 2025) has the clearest mechanism in this literature. A sketch model turns a natural-language proof into a lemma-style Lean sketch, and each lemma is then attacked in parallel by a prover. What happens on failure is the design. There are two distinct failure signals, and they trigger two distinct responses. If a lemma exhausts its budget without being proved, it was too hard, so the system goes deeper, generating a fresh natural-language proof and a fresh sketch for that lemma alone and turning a leaf into an internal node. If instead a lemma is disproved, the plan was wrong rather than hard, so the system goes sideways, returning control to the parent for a new decomposition. Recursion runs to depth four; the whole run then restarts from scratch with every lemma proved so far injected into the Lean context, which makes the effective depth eight. Reassembly needs no separate stitching step, since the sketch model must write a genuine main_proof body at every node before any child is attempted.
The scale of such a run is concrete. On the 2025 olympiad problems the reported per-problem solve times are \(0.01\), \(1\), \(5\), \(8\) and \(16.5\) hours, with the sixth problem unsolved. The figure usually quoted for this system is the slowest of these, and that the fastest was handled by a separate geometry solver rather than by the prover. A day on one theorem, then, is not a figure of speech.
Now the part I find genuinely surprising. The sketch model is the most important component in the system, since everything downstream is conditioned on the decomposition it proposes, yet it sits above the verification frontier, because a sketch full of sorry compiles. It is therefore trained against a rubric, described in the paper as an “LLM-as-a-Judge Rubric” acting as “a semantic value model”, with explicit vetoes on hollow bodies that delegate everything to their children. In a domain equipped with a perfect oracle, the component that matters most is supervised by a neural judge. That is not a compromise anyone made by preference; it is what Section 5 forces.
The other branch of this family makes the search explicit rather than recursive. Aristotle runs a Monte Carlo Graph Search over Lean proof states. The AND/OR structure makes proof search a minimax problem, so it takes an upper confidence bound on actions and a lower confidence bound on states. Each goal is additionally augmented with its logical negation, so budget can be spent on disproving it. That sentence names every component and specifies none of them, since there is no exploration formula, no backup rule, no pseudocode and no hyperparameter anywhere in the paper. It is precise enough to tell you what was built, and far too thin to let you build it. We will come back to what else it does not contain.
One correction in passing, because this family’s best-known member is often miscited. DeepSeek-Prover-V2’s subgoal decomposition runs at training time, where it manufactures cold-start chain-of-thought data from verified decompositions; at inference the large model does plain i.i.d. whole-proof sampling, with no search, no state and no adaptation. By the columns of our table, then, it belongs in the second family rather than this one. Its PutnamBench figure is \(47\) of \(658\) rather than the \(49\) that circulates, two statements having been withdrawn as misformulated.
Where this family stops is the formalisation tax. Every problem must be restated in the kernel’s language before any of this applies. That means human labour, the risk that a formal statement quietly fails to capture the informal one, and a restriction to the mathematics current libraries can express. That tax is what keeps the family narrow, and it is the price of being the only family whose progress genuinely adds up.
The environment as memory
The fourth family is cruder than the third and works better than it has any right to, because the state is a single document and the subagents share nothing else.
AlphaProof Nexus (Tsoukalas et al. 2026) describes its basic agent as a “Ralph loop”, and the loop is something one could write in an afternoon. A frontier general model is given a Lean file containing the target theorem and the regions it may edit. It reasons, edits the file with a search-and-replace tool, and the compiler checks the result; errors then steer the next turn. When an episode ends with the proof incomplete, the agent appends a comment summarising what it learned, and that file becomes the input to the next episode. Independent copies of the loop run in parallel with no shared state.
Nothing was trained for any of this. The paper uses a general model off the shelf. Its closing sentence then draws the conclusion I would have hesitated to draw for it: the results “point to an ongoing shift from specialized trained systems toward simple agentic loops as LLMs become more capable”.
The results are what make this more than a curiosity. Run on formalised open problems from the Erdős problems collection, the agent resolved nine. For comparison, AlphaProof itself is a reinforcement-learned prover with tree search. Run standalone at roughly 64 TPU-hours per problem, it solved none of the nine. An off-the-shelf commercial coding agent, pointed at the same problems in a mode where it keeps working toward a compiling proof, solved seven. Lest that suggest any model will do, a second commercial agent solved none, and variants of the loop built on smaller models also solved none.
There is a nuance here that is easy to overstate in either direction. The paper’s full system wraps the basic loop in an evolutionary framework coordinating subagents. What does that buy? On two of the nine problems it beats the basic loop with two to five times the monetary saving, while on the remaining seven it is, in the paper’s words, “roughly half as cost-efficient”. Those two problems happen to be exactly the two that the off-the-shelf agent could not solve. So the elaborate machinery is neither useless nor free: it earns its keep at the top of the difficulty range and costs roughly a factor of two everywhere else.
The store here is a file rather than a lemma library, which means the state does not transfer between problems, and each new theorem starts from an empty document.
Moving the weights
Four families keep the policy fixed during the attempt. The last one does not, and it completes the ladder at its fourth rung.
TTRL (Zuo et al. 2025) manufactures a reward where no label exists: sample many answers to a test question, take the majority answer as a pseudo-label, and run reinforcement learning against it. The obvious objection is that this should simply amplify whatever the model already believed, errors included, and the reason it does not is worth understanding. Label accuracy and reward accuracy come apart. On AIME 2024 the majority vote starts out picking the right answer about \(37\%\) of the time, while the reward signal derived from it is correct about \(92\%\) of the time. The reason is that when the pseudo-label is wrong, every sample disagreeing with it is still correctly marked wrong, since it also disagrees with the truth. One bad label bit thus becomes many mostly-correct reward bits, and only the second quantity ever reaches the gradient.
The granularity, however, is coarser than the framing suggests. Adaptation is per benchmark rather than per instance, since the weights persist across all the test questions and the evaluation happens on those same questions. This is a specialist for a distribution, not a specialist for a theorem.
The targeted variant, test-time curricula (Hübotter et al. 2025), gets closer to the latter. Given a target problem, it assembles a curriculum of related tasks and trains on them before attacking the target, which raises the question of where those tasks come from, since generated problems would have no ground truth. The answer is that they are retrieved from an existing corpus rather than generated, so every item arrives with a golden answer or a set of unit tests already attached, checked by one of a handful of shared verifiers. That dissolves the problem neatly, at the cost of capping the method at the coverage of whatever corpus is being searched. Much of the headline gain also turns out to be generic reinforcement learning on the corpus rather than targeting. Against a matched baseline trained on a thousand uniformly sampled tasks, the baseline recovers between \(56\%\) and \(83\%\) of the gain on their main backbone, depending on the benchmark. Across their other two backbones the share runs from \(13\%\) to over \(100\%\), and the upper end means the untargeted baseline simply won.
This is the most durable state in the table and the least controlled result, since no study here isolates the mechanism against a matched-compute arm that does not adapt.
What we actually know
Having walked the families, sort their claims by how well supported they are. I found the exercise more sobering than expected.
Several things look solid, in the sense of being measured directly or corroborated across independent papers. Reinforcement learning against a verified answer produces long chains of thought and lifts single-sample accuracy. Coverage scales log-linearly in the number of samples, while selection does not scale without a hard verifier, so \(\Gamma\) stays wide. A kernel plus decomposition reaches horizons that a single trajectory does not. And a frontier general model in a compile-check loop closes genuinely open problems.
A second tier is claimed without support in the paper making the claim, and here I would encourage some scepticism.
Aristotle’s abstract reports “state-of-the-art performance with favorable scaling properties for automated theorem proving”. Yet the paper contains no benchmark table, no benchmark numbers at all, and across twenty-three pages not a single percentage sign. There are two figures, both diagrams, and no plot of any kind, so there is no scaling curve to accompany the scaling claim. The only number resembling a result is five out of six. None of which makes the architecture uninteresting; it simply means the headline has nothing behind it that a reader can inspect.
Kimi argues that explicit search is unnecessary, ablates four other things instead, and obtains its best number through an outer search loop. Seed-Prover makes architectural claims with no controlled comparison isolating any component, and discloses no model size, no GPU count and no wall-clock for its competition runs, which leaves every baseline comparison unnormalised.
There is a third failure mode that is not in the papers at all. Seed-Prover is widely cited as having achieved a certified silver medal with 30 points at the 2025 olympiad, yet the words “silver”, “medal” and “30/42” appear nowhere in its body. What the paper claims is four problems by the submission deadline; it notes a fifth was finished afterwards and never mentions the sixth at any point. Since four complete problems is 28 points, the circulated figure implies partial credit the paper does not describe. The number comes from a company blog post instead. This is a lesson about provenance rather than about that system, and I include it because I repeated the claim myself before checking.
The pattern here is not carelessness, I think, but the absence of shared evaluation. No two systems in our table were run at matched compute on a common benchmark, so architectural claims survive without ablations because nothing forces the comparison.
The most interesting tier, though, is what nobody has tried. Plan-level verification that is not a neural judge. Lemma libraries that transfer between problems, given that every system we have seen starts each new theorem with an empty store. Closing the informal-to-formal loop without human formalisation. And any controlled comparison of these five families at matched compute, which would settle a surprising number of open arguments at once.
A dispute that dissolves
One question in this literature gets more attention than any other. Does reinforcement learning create reasoning capability, or does it only concentrate probability mass on solutions the base model could already produce given enough samples?
Both positions are published and both are credible. One side (Z. Chen et al. 2025) finds that base models match or beat their RL-trained descendants once \(k\) is large enough, which would make RL an elicitation procedure rather than a capability-creating one. ProRL (Liu et al. 2025) finds the opposite, reporting problems where prolonged RL reaches solutions that extensive sampling from the base model never finds.
The dispute is more tractable than it looks, because ProRL released the per-benchmark pass@\(k\) curves behind its claim. Reading the data labels off those figures is instructive. On AIME 2025 at \(k=256\), the base model scores \(0.704\) against ProRL’s final model at \(0.665\); the base model starts well below the trained model at \(k=1\) and finishes above it. That is the sceptical paper’s result, sitting inside the affirmative paper’s own appendix.
Across the figures I was able to read, the pattern is a split by domain rather than by method. On the real mathematics and coding benchmarks, the base model wins at large \(k\). On the synthetic puzzle tasks drawn from the training distribution, which the base model has essentially never seen, the trained model wins and often by a lot.
ProRL states the reconciling law itself, and prominently: it appears in the abstract, the introduction, a section of its own and the conclusion, always as the observation that gains are largest where the base model’s pass@128 is lowest. No correlation coefficient or fitted statistic accompanies it, only a scatter plot with a line through it. What the paper never does is connect the observation to the argument it is having. Reinforcement learning expands the reachable set where the base model had almost no mass to begin with, and redistributes mass where it already had plenty; competition mathematics sits firmly in the second regime. Both papers are right about their own domains, and the question was posed at the wrong grain.
I should be honest about the limits of that check. Most of the fifty figures resisted machine reading, so the domain pattern above rests on a handful of confirmed cases together with the regression the paper reports itself. It is a careful read of published plots, not a reanalysis.
The constraint underneath
Looking back at the five families, they are all workarounds for the same thing.
The first avoids decomposition entirely, so it never has to value a plan, and pays by stopping at the context window. The second decomposes nothing and pushes the whole problem into selection, where \(\Gamma\) is the tax. The third decomposes, then discovers that the kernel cannot score a decomposition, and trains a neural judge anyway. The fourth lets a compiler and a document stand in for valuation, and works better than it should. The fifth moves the weights instead of valuing anything.
The constraint is this. Hard verification is defined only on finished artifacts, so the decision that matters most in a long run, which is how to break the problem apart, is the one decision no oracle can score. Perfect verification at the leaves buys no verification of the plan.
This is also why compute compounds where it does and nowhere else. Durable state requires checking, checking requires finished artifacts, and so the only state that compounds is state reduced to something checkable. A proved lemma qualifies; a promising direction does not.
If I had to guess where effort pays, I would order it roughly as follows. Any trustworthy signal above the verification frontier would be worth more than everything else on this list, since it is the binding constraint in all five families. Lemma libraries that transfer across problems come second, because composability is the one property that makes compute accumulate and nobody currently exploits it beyond a single theorem. Reducing the formalisation tax comes third, since that is what keeps the only additive family narrow. Treating test-time weight updates as a first-class axis, with the controls nobody has run, comes fourth. And finally, the field is a collection of ad hoc responses to the single fact that generation is hard while checking is easy, which suggests room for a more deliberate exploitation of that asymmetry than anyone has attempted.
What I take from all this is a fairly simple diagnostic. Given a new system, ask what its hard verifier accepts, ask what survives when its context window closes, and ask which component sits above its verification frontier without an oracle. The first answer bounds what the system can learn from. The second bounds how long it can usefully run. The third is where it will fail, and it is almost always the part the paper describes with the most confidence.