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: an outcome reward model scores a whole solution, a process reward model scores each step (Lightman et al. 2023). Either makes best-of-\(n\) selection possible at inference, and DeepSeekMath-V2 trains a verifier for whole informal proofs, with a second model checking the verifier.

🚧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 well down the leaderboard, below a minimal scaffold around an unmodified Claude Opus that scores several 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, more than tripled its base model’s score on live Putnam 2025 in the same harness. 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 still need the statement in Lean, but formalize their own intermediate lemmas as they go.

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

Some maths specialists ship a reward model alongside the policy: a second model that reads a candidate solution and scores how likely it is to be right. AceMath (Liu et al. 2025) and Qwen2.5-Math (A. Yang et al. 2024) both do. With one, we can sample \(n\) candidates, score each, and return the highest-scoring; this is best-of-\(n\), reported as rm@n.

Whether that beats maj@k depends on the reward model. AceMath’s benchmark compares them at \(n = 8\): the maths reward models from AceMath and Qwen beat majority voting, while general-purpose reward models, including ones that rank highly on general reward benchmarks, do worse than counting. Ranking also costs more than the \(n\) suggests, since every candidate needs a pass through the reward model as well. I still have no idea how we would get a reward model we could trust on problems unlike its training set; trained verifiers has the open questions, and claim checking is one way to do without one.

A reward model can also grade each step rather than only the result, which makes it a process reward model (Lightman et al. 2023). The step scores are combined into one score per answer, so selection is still over whole answers. Step scores also allow selection during generation: extend the partial solutions whose steps score well and drop the rest, a beam search over reasoning. Particle filtering (Puri et al. 2025) makes that probabilistic, resampling partial solutions in proportion to their scores instead of keeping only the top few, which the authors argue makes the search harder to game through errors in the reward model.

It was widely guessed that OpenAI’s o1 used a learned verifier this way at inference, but OpenAI has never said so, and the open reasoning models point the other way. DeepSeek-R1 (DeepSeek-AI et al. 2025) reports trying process reward models and tree search and abandoning both, and gets its test-time scaling from one long chain of thought trained with RL.

4.5 Whole informal proofs — judged, not counted

A proof is a long, structured argument. Deciding whether a proof is right is hard, and deciding whether two proofs are “the same” is ill-defined, so we cannot vote over proofs, only over their conclusions. Instead, we can ask an LLM to judge each proof.

Nomos is an open harness from Nous Research built this way, released with nomos-1, a fine-tune of Qwen3-30B-A3B-Thinking-2507 for writing informal proofs. Parallel workers write proofs and have a judge score each out of 7, until every problem has four perfect scores or the time limit runs out. The harness then sorts the proofs by conclusion and keeps the group it judges correct, which need not be the largest, and picks one proof from that group by a single-elimination tournament of pairwise comparisons. By default nomos-1 writes the proofs, scores them, sorts them and referees the tournament, so every verdict in the pipeline is the model’s opinion of its own work. The one published evaluation is Putnam 2025, graded by a human expert: 87/120, against 24/120 for the base model in the same harness.

DeepSeekMath-V2 (Shao et al. 2025) trains the judge instead of prompting one. Its verifier learns to list the issues in a proof and score it 0, ½ or 1 against a rubric, and a meta-verifier checks that the issues it lists are real, which cuts down on invented flaws. The generator is then trained with that verifier as its reward, and is also rewarded for a self-assessment of its own proof that agrees with the verifier’s. With enough test-time compute it reaches gold-medal scores on IMO 2025 and CMO 2024 and 118/120 on Putnam 2024. That Putnam score is not comparable with Nomos’s: it is a different year, graded by DeepSeek’s own experts, from a model built on the 685B-parameter DeepSeek-V3.2.

4.6 Claims and errors

Instead of grading a whole attempt, we can grade one piece of it: a single claim in a worked solution, or the step at which a proof fails to compile.

On the final-answer side, the pieces are the claims an answer rests on. VibeThinker-3B’s Claim-Level Reliability Assessment (Xu et al. 2026) has the model check the key claims in each of its sampled solutions and discount the votes of solutions whose claims fail, which lifts its AIME26 score from 94.3 to 97.1.

On the formal side the compiler already does this, in a sense: it passes or fails the whole proof, but its error trace points at the step that broke. Iterative refinement uses that: generate, compile, feed the errors back, retry. 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.

The two use the piece differently. Claim checking runs its attempts in parallel and uses the verdicts to weight a vote; refinement runs them in sequence and uses the error to write a better next attempt. Specific feedback is what makes a retry worth more than another independent sample.

4.7 Lemmas — decomposing the theorem

The first open provers, DeepSeek-Prover and Goedel-Prover, were a fine-tuned model sampled many times, with at most a round or two of self-correction. They have since slid down the PutnamBench leaderboard (Tsoukalas et al. 2024) until they are the baseline everyone else beats. One way past them is recursive decomposition: break the theorem into sub-lemmas, prove each, reassemble, and recurse on whatever will not close. At the other extreme, tree search grows the proof tactic by tactic and consults Lean after every step; AlphaProof is the flagship, at 56% of PutnamBench. For now, systems that write a whole proof, or a whole lemma, and then compile it lead the leaderboard (Requena et al. 2026).

Apple’s Hilbert (Varambally et al. 2026) is the clearest open example. It splits the job four ways: a generalist reasoner does the informal maths and sketches a proof full of sorry holes, a Lean specialist (Goedel-Prover-V2-32B) closes the atomic goals, a retriever searches Mathlib, and the compiler verifies. With Gemini 2.5 Pro as the reasoner it solves 462 of 660 PutnamBench problems; with gpt-oss-120b as the reasoner and the same prover, it solves 88. 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) has the same plan-then-prove shape with more machinery, and Harmonic’s Aristotle (Achim et al. 2025) pairs informal lemma planning with a tree search; both reached gold-medal-equivalent scores on IMO 2025 in machine-checked Lean.

Decomposition is not the only route, though. Requena et al. (2026) put an off-the-shelf Claude Opus in the plain compile-and-retry loop, with no decomposition and no fine-tuning, and it solves 54.7% of PutnamBench at pass@1 for about $12.60 a problem. That is roughly level with Hilbert at pass@1, on a tiny fraction of the tokens. Without the loop, the same models manage about 5% at pass@20. Hilbert’s extra compute buys the last stretch: at pass@1840 it reaches 70%.

Decomposition also brings autoformalization into the loop. The benchmarks supply the theorem already in Lean, but not the lemmas; those come from the informal plan, are formalized one at a time as they are needed, and are revised whenever one fails to compile.

If the loop is doing this much of the work, how specialized does the model underneath need to be?