AI reasoning and proofs

2.1 What follows from the target

Three things depend on the target alone, whatever the model’s specialization.

How it can be checked. A final answer to a new problem cannot be checked directly. The best mechanical test is to ask a computer algebra system whether two candidate answers agree, which is a heuristic and provably incomplete. An informal proof has no mechanical checker at all; it is graded by a reader, either another model or an expensive human, and the verdict is an opinion. Call that a soft verdict. A formal proof has a compiler, and the verdict is exact. Mathematics is unusual in that the same theorem can be posed in all three forms, so we get to choose which kind of verdict we want; in most domains there is only one.

How many samples are worth drawing. For a final answer, the standard trick is majority voting, maj@k: draw \(k\) samples and return the most common answer. That converges on the mode of the model’s answer distribution, and the mode is either right or wrong, so after a few dozen samples more compute only estimates the same mode more precisely. For a formal proof we instead measure pass@k, whether any of \(k\) samples compiles. One compiling proof ends the search, and a wrong sample costs tokens and nothing else, since wrong candidates do not change the compiler’s verdict on the right one, so pass@k only ever improves with \(k\). That is why prover loops sample thousands of candidates while voting systems stop at a few dozen and spend the money on a better judge instead; more on this in the harness notes.

Whether votes can be counted at all. \(k\) final answers can be compared, and the most common one taken. \(k\) proofs cannot: two proofs of the same theorem are two different arguments, and there is no mode to take. So voting over proofs counts at most their conclusions, never the reasoning. A proof-emitting model needs either a compiler, as for Lean, or a judge that reads the arguments.

The target does not settle everything. Most models cannot write Lean at all, but among those that can, whether to use a generalist or a specialist is still open, and so is what the loop should remember between attempts.

3.1 Reinforcement learning from verifiable rewards

RLVR rewards the model for a checkably correct answer, so the checkability of the target matters here as much as at inference. RLVR needs a reward it can trust across millions of rollouts. A soft judge can be gamed by the policy, which we call reward hacking; a compiler cannot. That is why the formal target is as attractive for training as for inference, and the open specialist provers were made by expert iteration: train on the proofs the model just found, sample again, repeat.

RLVR costs capability in two ways. One is ordinary catastrophic forgetting: the model gets worse at other domains. That is a generic post-training problem rather than a mathematical one, and I leave it to others. The other, diversity collapse, is narrower and worse for our purposes.

🚧TODO🚧 the mechanics: GRPO and relatives, what the recipes actually look like, and how reward hacking shows up when the verdict is not exact.

3.2 Diversity collapse

RLVR concentrates probability mass on high-reward trajectories, which is what the objective asks for. The measured consequence is that RLVR models beat their base model at small \(k\) while the base overtakes them at large \(k\) (Yue et al. 2025). That is, RL made the model more likely to find the answers it could already find, at the cost of the range of answers it could find. ProRL disputed this, claiming that prolonged RL expands the set of solvable problems, but at \(k\) up to 8192 the set of problems the RL model lost was about three times the size of the set it gained (F. Wu et al. 2025).

This undermines the main advantage of the formal target, that we can sample thousands of times, and it has been measured on Lean. Kruszewski et al. (2025) train a 7B prover on Lean Workbook and trace the precision–coverage trade-off out to pass@256. GRPO gives high pass@1 and low coverage, and on one problem collapses to sixteen identical proofs that the base model already found likely. A prover does not want a correct proof, it wants diverse attempts, because a hard theorem may be reachable only through a rare derivation.

So the two kinds of leaderboard measure opposite ends of one trade-off. AIME-style boards report pass@1 or maj@k; PutnamBench entries run at pass@184, pass@1024, pass@1840. A post-training run that trades coverage for precision looks like an improvement on the first board and a regression on the second. No paper I know of reports both numbers for the same model.

The obvious fix, mixing more varied data into the training curriculum, does not work. The KL penalty in the standard GRPO objective is reverse KL, which is mode-seeking: it bounds how far the policy drifts from the base but does not stop it collapsing onto a subset of what the base already did. Much of the field (DAPO, Dr.GRPO) removes the penalty anyway, on the grounds that long-chain reasoning needs to drift a long way. Li et al. (2025) show that replacing the reverse KL with a mass-covering divergence prevents collapse, while replaying extra data into the gradient makes collapse worse. What matters is which distribution we anchor to and which way the divergence points, not how much data we mix in.

Hochlehnert et al. (2025) arrive at the same practical advice from a different direction. They ask how much of the published progress survives a standardized evaluation harness, and find that most RL gains are modest and overfit to small benchmarks, while supervised fine-tuning generalizes more consistently. Both lines of work say to prefer the SFT checkpoint.

🚧TODO🚧 The measured mixtures all anchor to the model’s own distribution, so whether replaying general, non-mathematical data preserves high-\(k\) coverage within mathematics seems to be unmeasured.

3.3 Trained verifiers

When no checker exists, we can train one. Process reward models grade the steps of a solution rather than its conclusion (Lightman et al. 2023). They make best-of-\(n\) selection possible at inference, and DeepSeekMath-V2 trains the policy to grade itself the same way.

🚧TODO🚧 how they are trained, how they are fooled, and whether a verifier trained against known answers is any use on novel mathematics, where there are none; the practical version of that question.

3.4 Does narrow specialization pay?

The evidence looks mixed until we sort the specialists by size.

The large specialists do badly and the small ones do well. That looks like one finding, but it is three, each with a different standard of evidence.

For formal proofs, large specialists lose, and the measurement is clean. Within one paper under one protocol, Goedel-Prover-V2-8B beats DeepSeek-Prover-V2-671B on MiniF2F at the same pass@32, despite having 84× fewer parameters. On PutnamBench both big fine-tunes are now around rank 15 of 39, below a minimal scaffold around an unmodified Claude Opus that scores four times DeepSeek-Prover’s total at pass@1 rather than pass@1024.

For final answers, the comparison has never been run. No large maths specialist, not Qwen2.5-Math, OpenMath-Nemotron, AceMath or Skywork-OR1, has been scored beside a frontier generalist under a shared, independently-run protocol. MathArena, the one platform that runs everything through an identical harness, has evaluated none of them. Every table that seems to compare them puts specialist numbers from the specialist’s own 2024–25 paper (greedy or avg@64) beside frontier numbers from a 2026 vendor blog post at an undisclosed protocol, possibly with tools on. I think the large specialists lose, but I cannot show it, and neither can anyone else.

Small specialists do well, but only on the kind of problem they were tuned for. VibeThinker-3B (Xu et al. 2026) (weights) reports AIME26 94.3 against DeepSeek V3.2’s 94.2 with 224× the parameters, a gap of one thirtieth of a problem, i.e. no gap at all³. nomos-1, with 3B active parameters, scored 87/120 on live Putnam 2025, blind-graded by a human, where the same base model in the same harness scored 24/120. The qualifier matters, and QED-Nano shows why. It is the only small specialist that has been run through a common harness; it manages 82.5% on AIME 2026 and then 14.06% on ArXivMath, last of twenty-seven, for an overall rank of 67 out of 94. Tuning for AIME generalizes to AIME. Few people check this: Qwen2.5-Math and OpenMath-Nemotron publish no general benchmark at all, only a model-card note advising against using the model for anything else.

Those AIME figures are also self-reported, and the one independent measurement of a VibeThinker model comes in lower than the headline. Hochlehnert et al. (2025) re-run the open reasoning models under a single harness across ten seeds with error bars, and find most published gains are within the noise; a thirty-problem benchmark routinely gives ±4 to ±7 points. Their VibeThinker-1.5B scores 75.7 ± 3.9 on AIME24 and 71.3 ± 7.7 on AIME25. That is a smaller model than the 3B quoted above, so it does not contradict the 3B’s numbers; it is the only third-party evaluation of the family. They evaluate only open models between 1.5B and 32B, no frontier generalists and no large specialists, so they do not settle the comparison above either.

VibeThinker’s authors explain this as a split between compression and coverage: verifiable reasoning can be compressed into few parameters, while open-domain knowledge and long-tail understanding are what consume parameters. Their own table shows both halves: AIME parity with models two hundred times larger, next to GPQA-Diamond 70.2 against Gemini 3 Pro’s 91.9. If that holds, the mathematical part of a maths system is the cheap part, which is also what the decomposition systems found from the other direction, and the niche for a specialist is wherever we need many cheap calls.

3.5 Training a model for its harness

The nomos-1 and QED-Nano results can be read another way. Both models were post-trained for a specific loop, and both were then scored inside that loop against their own base model: same harness, different model. That measures how well the model responds to its scaffold, not raw mathematical ability, and no leaderboard measures it. It also means those two numbers cannot settle the question above. A model tuned for mathematics and for a harness, evaluated in that harness, does not tell us which half of the tuning helped. Nobody has published the ablation.

4.1 CoT and TIR

Solvers that emit final answers come in two kinds.

CoT (chain-of-thought) solvers just think reeeeealllly hard. Everything uses a chain of thought somewhere; CoT solvers do nothing else, and are bareback, totally normal LLMs applied in a nerdy way.

TIR (tool-integrated reasoning) solvers use tools. The model writes mathematical code, usually Python, runs it, reads the result back and carries on, self-correcting any wordcel errors with the help of its shape-rotating software stack. TIR models need a harness that gives them a code interpreter and feeds the output back, so a generic harness will not drive one.

4.2 Proving with a compiler in the loop

Here the target is a formal proof. Each iteration, a model emits a candidate Lean 4 proof, the compiler either accepts it or returns an error trace, and we either keep the proof or feed the error back and retry. Two things follow from the checker being a compiler in particular.

• The checker works on any problem, including ones nobody has seen before, unlike a trained verifier. Because the loop can run as long as we like, a published prover score is a score for a model plus its sampling-and-refinement budget, and comparing two provers means comparing two loops.
• The mathematics the model may cite is versioned. Lean’s formalized mathematics is collected in Mathlib, an enormous communal library, and every proof is assembled from it, so the Mathlib version is part of the harness rather than a detail.

A prover also needs a formal statement to attack, and most mathematics is not written in Lean, so a pipeline starting from English needs autoformalization first: a model that turns the English statement into a Lean one. Autoformalizers are much less reliable than the provers they feed. Specialists exist (Herald (Gao et al. 2025)) but are not widely available, so the usual dodge is to start from a hand-written formal statement, as the benchmarks do. Decomposition systems avoid the problem differently, by formalizing one lemma at a time.

4.3 Whole answers — maj@k

The simplest test-time-scaling trick (X. Wang et al. 2023): draw \(k\) independent samples at non-zero temperature⁵, return the most common answer. One limitation we have already met: the most common answer may be wrong. A second is that we need to be able to tell when two samples gave the same answer. For a boxed integer we can. For an expression we must ask a computer algebra system whether two expressions are equal, and that is undecidable in general for expressions built from \(\exp\), \(\log\), \(\pi\) and friends, by Richardson’s theorem (Richardson 1968), so any simplify is a heuristic with an inexhaustible supply of counterexamples. There are more mundane failures too: LaTeX is a typesetting language rather than a syntax, so parsing can fail before the mathematics starts, and one sample may write \(\sigma_1\) where another writes \(s_1\) for the same quantity.

So the vote-counting step is itself a soft verifier. The question moves from is this answer right to is this answer the same as that one, but it is still a judgement call, and the usual fix is an LLM judge, with all the unreliability that brings. Pass@k has no such step, because the compiler judges each candidate alone and there is nothing to compare. In practice this costs a lot.

4.4 Whole answers, ranked — best-of-n

When a model ships a reward model alongside the policy (AceMath does (Liu et al. 2025); some specialists do not), we can do better than plain voting: sample \(n\) candidates, score each with the reward model, return the highest-scoring. Best-of-\(n\) against a calibrated verifier beats maj@k for the same compute budget, because the verifier carries information about which sample is right, not just which answer is most common. Easy to say, but I have no idea how we would get such a reward model in general, nor why I should trust it.

The most famous instance at scale is OpenAI’s o1 and successors, which reputedly use a learned verifier (Lightman et al. 2023) to do beam-search-like selection of reasoning traces inside the chain-of-thought; see s1 (Muennighoff et al. 2025) for an open replication and the probabilistic inference scaling work (Puri et al. 2025) for the formal framing.

4.5 Whole informal proofs — judged, not counted

When the output is a proof rather than a value, votes can only count conclusions, so instead of counting we need a judge that reads the candidates.

Nomos is an open example. Nous Research released nomos-1, a Qwen3-30B-A3B-Thinking-2507 fine-tuned to write proofs in natural language, no Lean anywhere, alongside the harness it was tuned to run inside. Workers sample proofs in parallel against a judge prompt; the finalizer then groups submissions by conclusion, keeps one group, explicitly not necessarily the largest, and runs a single-elimination tournament among the survivors. Grouping by conclusion recovers the tally a vote would have counted, but the finalizer does not treat the tally as evidence, since a pile of agreeing wrong proofs is a normal failure for a maths harness.

Nothing in it is exact, though: the judge defaults to nomos-1 itself, so the same model writes the proofs, scores them and referees the tournament. On Putnam 2025 the combination scores 87/120, graded by a human expert. That is self-reported, on one benchmark, and not comparable to a PutnamBench figure, which is graded by a compiler. A specialist judge beats a generalist at reading proofs, but it is still only a judge.

4.6 Claims and errors

At this level both the final-answer and proof systems stop grading the whole submission and start grading pieces of it.

On the final-answer side, one way to get the reward model of the previous section is to have the policy grade itself: draw \(k\) trajectories, split each into a few decision-relevant claims, have the model verify each claim, and weight each trajectory’s vote by how many of its claims hold, so an answer reached through a broken step counts for less than the same answer reached cleanly. DeepSeekMath-V2 (Shao et al. 2025) does this at large scale, lifting AIME26 from 94.3 to 97.1; VibeThinker-3B’s Claim-Level Reliability Assessment (Xu et al. 2026) does it at small scale.

On the formal side the equivalent is iterative refinement: generate, compile, feed the errors back, retry. The unit being checked is an individual error rather than the whole proof. The minimal-agent ablations (Requena et al. 2026) find this the single largest driver of success, ahead of model choice, tools, or memory; Goedel-Prover-V2’s two-round self-correction is the same thing.

Both of these run attempts in sequence, where the methods above run them in parallel. Checking a finer unit gives the feedback something specific to say, and specific feedback is what makes a retry worth more than another independent sample.

4.7 Lemmas — decomposing the theorem

Until early 2025 a prover was one fine-tuned model plus one retry loop. Those models, DeepSeek-Prover and Goedel-Prover, have since slid down the PutnamBench leaderboard (Tsoukalas et al. 2024) until they are the baseline everyone else beats. What tops the scores now is recursive decomposition: break the theorem into sub-lemmas, prove each, reassemble, and recurse on whatever will not close. There is an even finer unit: tree search grows the proof tactic by tactic and consults Lean after every step, with AlphaProof as the flagship. But methods that compile a whole candidate proof in one go have been winning (Requena et al. 2026), and decomposition is the best of them.

Apple’s Hilbert (Varambally et al. 2026) is a clear example. It splits the job four ways: a generalist reasoner does the informal maths and sketches a proof full of sorry holes, a cheap Lean specialist closes the atomic goals, a retriever searches Mathlib, and the compiler verifies. Their main finding is that the choice of reasoner matters more than the choice of prover: the maths specialist is the commodity part, and the generalist doing the decomposition is where the wins are. ByteDance’s Seed-Prover (L. Chen et al. 2025; J. Chen et al. 2025) and Harmonic’s Aristotle (Achim et al. 2025) have the same shape with more machinery, and the strongest of these have reached gold-medal-equivalent scores on IMO 2025 in machine-checked Lean. Requena et al. (2026) go further: an off-the-shelf Claude Opus in a plain compile-and-retry loop, with no fine-tuning at all, solves 54.7% of PutnamBench at pass@1 for about $12.60 a problem, four times DeepSeek-Prover-V2-671B’s total at a thousandth of its sample budget. The same paper also shows the limit of that: without the loop, the bare models manage about 5% at pass@20, worse than Goedel-Prover. The loop closes the gap, not the generalist.

Decomposition also brings autoformalization into the loop. The informal argument is the plan; it is formalized lemma by lemma and revised whenever a piece fails to compile, instead of formalizing the whole statement once, with 55–75% success, before proving starts.

If decomposition is doing the work, how specialized does the model underneath need to be?