Reasoning and proof models
Inference-time-scaling considered unreasonably accurate
2019-12-08 — 2026-07-27
Wherein Is Charted the Design Space of Mathematical Reasoning Systems—solvers, Provers, and Autoformalizers—noting That a Lean Compiler’s Exact Verdict Permits Sampling Budgets Into the Thousands, Unlike Majority-Vote Solvers.
Somewhere between computational symbolic mathematics, automated proof assistants and large language models, we find the models that solve mathematical problems. General-purpose LLMs do OK at this; we have spent the last few years working, with variable success, on specializations that do better.
This page is mostly AI slop, i.e. LLM descriptions of my decisions in some recent exploratory projects. However, it is useful, so I am publishing it now rather than waiting for a more polished version.
Amazing fact: next-token predictors like transformers can do symbolic reasoning, and critique of that reasoning, through chain-of-thought. This is some kind of magic. I do not know how much of the apparent reasoning is search, how much is memorization, and how much is “true” generalization. I do not know what the complexity-theoretic story is, and I could not say at what scale the ability appears, or why — though I know all these things are well researched. Let us take it as given: baseline mathematical competence is available in a good generalist LLM. (“Claude, what is the derivative of \(x^2\)?”) What we can add on top is a harness around the model that exploits the unusual features of mathematical reasoning — inference-time tricks, that is, rather than training-time ones like Reinforcement Learning with Verifiable Feedback, which are not covered here. This page is the shape of that design space; the build log is next door.
1 Why can transformers reason?
CoT, computational complexity, program synthesis etc. 🚧TODO🚧
2 What counts as an answer
Mathematics is an unusual domain in that sometimes things are clearly right or clearly wrong. Where that holds we get what looks like free supervision: sample a candidate, check it, feed the result back. Whether it holds is decided by a single choice — what we ask the model to emit — which I will call the target. Everything else follows from it in a fixed order: the target fixes what checker can exist; the checker fixes how far its verdict can be trusted; and how far we trust the verdict fixes how much machinery we can afford to build around it.
That order is the general argument about harnesses, whose vocabulary I borrow throughout this page. It is also why solver, informal prover and prover are names for positions along it rather than species of animal: almost everything separating them follows from the target, and none of it from either being cleverer.
What the model emits. Four things, in practice, under the names the field uses for them.
A final answer is what a solver emits: a chain of reasoning ending in a boxed answer, literally \boxed{42}, the LaTeX convention the benchmark graders scrape, carrying one final value — an integer, a closed form, a yes-or-no — and not the argument that arrived at it. The working is there to be read, but it is the boxed value that gets graded, which is what makes this target behave so differently from the two below. Nothing certifies that value as correct: a computer algebra system can tell us when two candidates agree, which is a different question, so voting and self-critique are the best on offer. Some solvers have additionally been tweaked to run symbolic maths tools to check their working, the so-called TIR sub-family.
An informal proof is a whole proof written out in natural language; an informal prover writes them. Informal is the field’s word, and it marks the language rather than the standard: an informal proof can be perfectly rigorous, and it is how essentially all human mathematics is written. That makes this the most interesting object here, because it is closest to the traditional mathematician’s workflow, and the hardest to check, annoyingly.
A formal proof is Lean 4, the ascendant proof assistant language, and a prover emits one for the Lean compiler to accept or reject. Unqualified, prover means this one throughout, as it does in the literature — Goedel-Prover, Kimina-Prover, DeepSeek-Prover and the rest all emit Lean. That verifier is exact rather than persuadable, which changes what the machinery around it can get away with, enough that it gets its own section.
A formal statement is what an autoformalizer emits from an English one, so that a prover has something to attack.
The same words label the problems, and that is usually where we meet them first: a benchmark is final-answer or proof-based (Dekoninck et al. 2026), and a proof-based one is informal or formal depending on who does the grading.
How specialized the model is. Most frontier language models are generalists, and mathematical reasoning is one of the things they are trained on. They do alright on AIME-style problems as a side effect of being “good at language” and following instructions and whatever else happens inside the labs, and we drive them with an ordinary agent harness — Claude in Claude Code, say. Then there is a narrower class: models hard-specialized on mathematical reasoning, which trade away chat fluency and agentic competence to get it. Qwen2.5-Math (A. Yang et al. 2024), OpenMath-Nemotron (Moshkov et al. 2025), Skywork-OR1, AceMath (Liu et al. 2025) are specialist solvers; Goedel-Prover (Lin et al. 2025), OProver (Ma et al. 2026), DeepSeek-Prover (Ren et al. 2025) are specialist provers.1
| emits ↓ · specialization → | generalist | maths specialist |
|---|---|---|
| a final answer (boxed) | Claude, DeepSeek, a big Qwen3-Thinking | Qwen2.5-Math, OpenMath-Nemotron, AceMath |
| an informal proof | Claude et al., asked nicely | Nomos-1 |
| a formal proof (Lean) | a frontier model inside a prover loop — current SOTA | Goedel-Prover, DeepSeek-Prover, OProver |
| a formal statement (Lean) | — | Kimina-Autoformalizer, Goedel-Formalizer, Herald |
2.1 What the target decides
The rows of that table are the target; the columns are not. Three consequences follow from the rows alone, and they are why the rest of this page is arranged as it is.
What can check it. Where the target is a final answer, nothing checks correctness directly, and the strongest mechanical check we have is a computer algebra system testing whether two candidates agree: better than an opinion, provably incomplete, and known as a heuristic-symbolic verdict. Where the proof is informal there is no mechanical checker at all, and the verdict is a reader’s opinion — another model’s, or an expensive human’s — which is soft, the weakest grade and the only one that can be argued with. Where the proof is formal the checker is a compiler, and the verdict is exact. No system enjoys more than one of these at a time; what is unusual about mathematics is that we get to pick which. The same theorem can be posed as a final answer, an informal proof or a formal statement, so the target is a free variable here where most domains hand us one and no alternative. That is why the consequences below are comparable at all, rather than something to be inferred across fields.
How far it pays to sample. The final-answer and the formal targets both sample wide, and both are right to: maj@k at \(k\) of 8 to 64 is bread and butter and it moves real leaderboards. What differs is where the returns stop, and why. maj@k converges on the mode of the model’s answer distribution, and that mode is either right or it is not — so past a few dozen samples the extra compute buys a sharper estimate of a fixed quantity rather than a better answer, and a confident systematic error is exactly the thing it cannot escape. Pass@k is non-decreasing in \(k\) by construction: one compiling proof ends the search, and a wrong sample costs tokens and nothing else, because no volume of wrong candidates talks a compiler round. So incorruptibility sets how large a sampling budget can usefully be, which is why prover loops run to the thousands while a voting system caps out early and the money goes into a better judge instead. That is why two maths systems can afford such different amounts of brute force, and it is not a fact about how clever either one is.
Whether aggregation exists at all. A set of arguments has no mode to take. Where the target is a final answer, \(k\) samples are \(k\) comparable objects and the mode is a signal; on either of the two proof rows, \(k\) samples are \(k\) arguments. So a proof-emitting model dropped into a voting loop gives us at most a vote on the conclusion, never on the argument that reached it: it wants a checker downstream — Lean, for Goedel — or a judge that reads the arguments instead of counting them, which is what the good informal-proof systems build.
What the target leaves open. It does narrow the field of models, and sharply — a Lean target excludes everything that cannot emit Lean, which is most things, VibeThinker among them. But among the models that clear that bar the target says nothing at all, and whether to fill the slot with a generalist or with something fine-tuned for the job is the live argument rather than a consequence of anything above. Nor does the target settle what a loop should remember between attempts, which is a build question with a surprisingly large answer.
2.2 Reasoning modes in solvers — CoT and TIR
Within the final-answer target, two classes: the ones that augment their reasoning with tools and the ones that just think reeeeealllly hard.
The latter are the CoT (chain-of-thought) models. Everything uses a chain-of-thought somewhere, but CoT solvers do nothing else; they are bareback, totally normal LLMs applied in a nerdy way.
The former are TIR (tool-integrated reasoning). 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. Everywhere else the harness constrains the model; here it runs the other way, and a generic harness will not drive one.
3 Proving theorems with a compiler in the loop
Here the target is a formal proof rather than a final answer. In each iteration, a model emits a candidate Lean 4 proof, the Lean compiler either accepts it or returns an error trace, and we either keep the proof or feed the error back to the model and retry. How far it pays to sample against such a verdict is covered above; two further things follow from the checker being a compiler in particular.
- The verifier is trustworthy on problems outside the training data, including ones nobody has seen. This is the
Pass@kregime — the chance that at least one of \(k\) samples compiles — and it is why a prover can be scored on problems its authors never anticipated. It also means a published prover number is a number for a model plus its sampling-and-refinement budget, so comparing two provers means comparing two loops. - The mathematics the model may cite is a versioned artefact. Lean keeps its mathematical knowledge in Mathlib, an enormous communal library of formalized results, and that is the bank any proof is assembled from — which makes the Mathlib version a load-bearing part of the harness rather than a detail.
A prover also needs a formal statement to attack, and most mathematics is not written up as Lean, so a pipeline starting from English needs autoformalization first — a model turning the sentence into a Lean statement, and a much less reliable model than the prover it feeds. Specialists exist (Herald (Gao et al. 2025)) but are not well commoditized. While the unit of checking is a whole proof, the usual dodge is to duck the question and start from a hand-written statement, as the benchmarks do. The dodge stops being necessary at the lemma rung, which is much of why the fine-grained systems work.
4 How finely we check
Extra inference compute buys better answers than a single shot — sample many candidates, combine them, and beat a much larger single-shot model — and the interesting variation is not how much we spend but what unit we spend it on.2
The rungs below differ in the unit a verdict is passed on — a whole answer, one claim inside it, one lemma, one tactic. Fine units are recent, and are where the proving frontier has moved. The two literatures climbed the same rungs a couple of years apart in different vocabulary.
| Unit checked | Final-answer side | Proof side |
|---|---|---|
| The whole thing | maj@k (soft), best-of-\(n\) against a verifier (soft, but trained) | judged, not counted (soft, informal), one-shot sampled wide (exact, formal) |
| A claim, or an error | claim-level reliability (soft) | iterative refinement (exact) |
| A lemma | — | recursive decomposition (exact) |
| A tactic | — | tree search (exact) |
The systems at the top of the proof leaderboards are at the bottom of the table; on the final-answer benchmarks the top is still the coarse rungs done well. The two columns run separately along the top rung, where they differ by grade rather than by unit, and meet at the second. Below that the proof column continues alone, and there only for the formal target, because only a cheap incorruptible verdict can be spent on fragments — which here means a compiler. A soft judge asked to grade a single tactic faces a question it can answer no better than it can grade the whole proof.
4.1 Whole answers — maj@k
The coarsest rung, and the simplest test-time-scaling trick (X. Wang et al. 2023): draw \(k\) independent samples at non-zero temperature3, return the modal value. This is called maj@k. It works, and the ceiling on it we have already met is that the mode may be confidently wrong. Here is the second one.
“Return the modal value” carries an assumption the formula hides — that we can tell when two samples said the same thing. For a boxed integer we can. For an expression we are asking a computer algebra system whether two things are equal, and zero-equivalence for expressions built from \(\exp\), \(\log\), \(\pi\) and friends is undecidable, by Richardson’s theorem (Richardson 1968), so any simplify is a heuristic with an inexhaustible supply of counterexamples. Below that ceiling sit two more mundane failures: LaTeX is a typesetting language rather than a syntax, so the parse breaks before the mathematics starts, and one sample may write \(\sigma_1\) where another writes \(s_1\) for the same quantity, which is not a mathematical question at all.
So the aggregation step is a soft verifier in its own right. maj@k does not escape the soft-verdict regime by being mechanical; it relocates the softness from is this answer right to is this answer the same as that one, and the standard remedy at that point is an LLM judge, which inherits everything that entails. Pass@k has no such step, which is a structural advantage of the exact verdict: the compiler judges each candidate alone, so there is nothing to cluster. Measured, in practice, this costs a lot.
4.2 Whole informal proofs — judged rather than counted
Where the output is an argument rather than a value, a vote can count conclusions but not reasoning, so the aggregation step has to become a judge that reads the candidates.
Nomos is a worked answer, in the open: Nous Research released nomos-1 — a Qwen3-30B-A3B-Thinking-2507 specialized for proof-writing in natural language, no Lean anywhere — alongside a harness it was tuned to run inside. Workers sample in parallel against a judge prompt, and then the finalizer 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 declines to count that as a signal: a pile of agreeing wrong proofs is a failure a maths harness can expect.
Nothing in it is exact, though. The judge defaults to nomos-1 itself, so the model writes the proofs, scores them, and referees the tournament between them. On Putnam 2025 the combination scores 87/120, graded by a human expert — self-reported, on one benchmark, and not comparable to a PutnamBench figure, which has a compiler where this has a grader; no cost per problem is published either, which leaves it on an ambiguous rung of the price ladder. A specialist judge beats a generalist reading prose, but it is still a judge.
4.3 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 — 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 of this trick at scale is OpenAI’s o1 and successors, which reputedly use a learned verifier (Lightman et al. 2023) to do beam-search-like reasoning trace selection inside the model’s 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.4 Claims and errors
This is the rung where the two columns meet: both stop grading the whole submission and start passing verdicts on pieces of it.
On the final-answer side the question is where the reward model of the rung above is supposed to come from, and one answer is that the policy grades itself. Confidence then attaches to each claim rather than to the final boxed answer, so the loop can say which steps to trust rather than only which answer won the vote. DeepSeekMath-V2 (Shao et al. 2025) is the large-model version; VibeThinker-3B’s Claim-Level Reliability Assessment (Xu et al. 2026) is the small-model one, which shows the move working at 3 billion parameters. Regardless of model size the process is similar: the loop draws \(k\) trajectories, splits each into a few decision-relevant claims, has the model verify each claim, and weights a 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. In the large-model case that lifts AIME26 from 94.3 to 97.1, which doesn’t sound like much but corresponds to a nominally much larger model’s performance.
On the formal side the same rung is iterative refinement: generate, compile, feed the errors back, retry. The unit being checked is an individual failure rather than the whole proof. The minimal-agent ablations (Requena et al. 2026) rank this as the single largest driver of success, ahead of model choice, tools, or memory; Goedel-Prover-V2’s two-round self-correction is exactly this.
Both are sequential wiring, where the rungs above are parallel. A finer unit of checking is what gives feedback something specific to say, and feedback is what makes iteration worth more than another independent sample.
4.5 Lemmas and tactics
Into early 2025 a prover was one fine-tuned model plus one retry loop. Not any more. The single model that emits a whole proof — DeepSeek-Prover, Goedel-Prover — has slid down the PutnamBench leaderboard (Tsoukalas et al. 2024) until it is the baseline everyone else beats. What tops the scores is now an agent, checking at the finest units available.
In Axiomatic AI’s taxonomy (Requena et al. 2026), provers split first into tree-search methods, which grow a proof tactic-by-tactic and consult Lean after each step (AlphaProof was the flagship), and whole-proof methods, which emit a candidate proof and compile it in one go. Whole-proof has been winning, and recursive decomposition — break the theorem into sub-lemmas, prove each, reassemble — is where the frontier sits.
The decomposition systems stopped being a single model some time ago. Apple’s Hilbert (Varambally et al. 2026) splits the job four ways — a generalist reasoner doing the informal maths and sketching a proof full of sorry holes, a cheap Lean specialist closing the atomic goals, a retriever over Mathlib, and the compiler as verifier — and recurses on whatever it cannot close directly. Which slot matters is the finding to keep: the choice of reasoner beats the choice of prover, so 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) are the same shape with more machinery bolted on.
This is where autoformalization stops being a front-end and moves inside the loop. At the lemma rung the natural-language proof is the plan: the informal argument is drafted first and formalized lemma-by-lemma, with formal failures feeding back to revise the informal sketch. So the statement is no longer a single 55–75% gamble taken once before the proving starts — it is a hypothesis under continuous revision by the same exact verdict that checks the proof. Draft-sketch-prove is the spine now, not an add-on, and that is how a finer unit dissolves a reliability problem the coarse ones had to live with.
None of these is a bigger prover we can rent by the token. Aleph from Logical Intelligence, Seed-Prover 1.5 and Aristotle are API-or-pilot-only, priced in dollars per problem rather than at a flat per-token rate, with Aleph’s runs estimated at $23–$68 each; the strongest of them have cleared gold-medal-equivalent on IMO 2025 in machine-checked Lean.4 The open-weight specialists we can download sit near the bottom of the same leaderboard, so what separates the frontier from the home practitioner here is a price rather than a download — priced against a home-built loop, in the build notes.
Which raises the obvious question — if refinement and decomposition are doing the work, how specialized does the model underneath need to be? The evidence points both ways.
5 Benchmarks and data
The benchmarks split by target, the same way the systems do, so the leaderboard a model appears on tells us what kind of thing it emits before we read any numbers.
Final-answer benchmarks grade a boxed number, which is the solver’s and the generalist’s game.
- GSM8K (grade-school word problems with integer answers) is totally MNIST, which is to say, a smoke test.
- MATH — people usually use the MATH-500 subset
- AIME (Mathematics Olympiad recruitment problems with integer answers 0–999) is more like ImageNet, i.e. it has some actually hard problems in.
Grading these is the equality problem again — a MATH answer is LaTeX, where \frac{1}{2} and 0.5 are both correct — so a benchmark harness ships a grader alongside the data, as NeMo-Skills does. These data sets are widely regarded as being mined out. The stringent moving benchmark in MathArena (Dekoninck et al. 2026) mitigates this problem by managing data contamination somehow? [TODO clarify]
Published scores on AIME / GPQA / MATH are also usually made from a diversified voting scheme — maj@k at \(k \geq 8\), temperature ≠ 0, often with the vendor’s own reward model in the loop (NeMo-Skills’ GenSelect (Moshkov et al. 2025), AceMath’s reward). A single sample at \(T = 0\) (i.e. classic chat style) will do much worse.
Proof-based benchmarks grade a whole argument, and they split again by who does the grading. The informal ones need a reader: IMO-ProofBench and MathArena’s proof-based competitions are scored by expert humans, or by models standing in for them, which is why Nomos’s 87/120 does not sit on the same axis as a PutnamBench number. The formal ones hand the proof to a compiler, which either accepts it or does not. MiniF2F (Zheng, Han, and Polu 2022) is the old smoke test — a few hundred Olympiad statements in Lean — and the strong provers have all but saturated it. The live target is PutnamBench (Tsoukalas et al. 2024), 600-odd Putnam problems formalized in Lean, where the leaders now solve most of the set and the very top is approaching all of it; FormalMATH (Z. Yu et al. 2025) is the bigger, broader follow-up. A machine-checked leaderboard handles contamination from the opposite end to MathArena: it does not much matter if the statement leaked, because a self-consistent wrong proof still fails to compile, so the score measures proving rather than recall. The same machinery is starting to grade code — VERINA (Z. Ye et al. 2026) and VeriSoftBench (Xin et al. 2026) ask a model to emit a program, a Lean specification, and a machine-checked proof that the two agree, carrying the compiler-as-verifier idea on from theorems to provably correct software.
6 The frontier is shifting
Two threads run through everything above, and both are still in motion.
The verdict has hardened. The final-answer end started with a majority vote — the softest verdict there is, one model’s opinion counted \(k\) times — and has been acquiring structure ever since: reward models, then per-claim grading, then models that carry their own verifier. The formal end started exact and stayed exact; what changed there was the discovery of how much brute force an exact verifier repays, and how fine a unit it can be spent on.
Specialization is the second thread, and it reads at first as a one-way street. The obvious story: the single fine-tuned model that emits a whole proof has slid down the open leaderboards; what beats it is a generalist wrapped in refinement, decomposition and search with a cheap specialist closing the atomic goals; so the maths model is becoming the commodity part. Requena et al. (2026) put Claude Opus in such a loop with no fine-tuning at all and landed competitively against the trained provers. Apple’s Hilbert found that the choice of reasoner mattered more than the choice of prover. Both of those look like the loop eating the model.
The counter-evidence arrives from the other side and is just as clean. Nomos-1 scores 87/120 on Putnam 2025 inside its own harness, and the Qwen3-30B-A3B-Thinking-2507 it was fine-tuned from scores 24/120 inside the same harness. QED-Nano reports the same shape at 4B: identical agent scaffold, twenty points over the base it was tuned from, while that base barely moves under the scaffold at all. VibeThinker’s Claim-Level Reliability Assessment is a third instance of it. Those look like the model eating the loop.
The two sets of experiments varied different things. The loop-side results held the model fixed and varied the harness; the model-side results held the harness fixed and varied the model. Each measured the thing it varied, and neither measured commoditization of the other. Between them they say the model and the harness are separately purchasable multipliers on the same problem, and that the multipliers compose — which is also why the systems at the top are co-designed, a model trained for a harness built for that model, and why none of them ships one half without the other.
So a proof system is turning from a kind of model into a kind of pair, which is worse news for the home practitioner than the commodity story was. A loop does get better for free every time the base model under it improves, and that part still holds. But the compounding only arrives when the model was trained to be looped, and responsiveness to a scaffold appears on no leaderboard: the only way to find it is to run the thing in our own loop and watch what happens.
None of which says the small specialists die. VibeThinker-3B (Xu et al. 2026) (weights) reports frontier-level verifiable maths and code from a 3B base, small enough to run on a phone, and its authors claim this as a compression-coverage split: verifiable reasoning compresses into a small core, while open-domain knowledge and general competence are what actually consume the parameters. If that holds, the mathematical part of a maths system is the cheap part and the expensive part is everything else the generalist knows — which is the decomposition systems’ finding arrived at from the other direction. It also puts a usable maths specialist at hobbyist scale rather than lab scale. A model that fits on a phone is a different kind of useful, and a 3B that responds well to a scaffold is precisely the model this argument says to want.
7 But is it OK to automate mathematics?
I have complicated feelings about this. On the one hand mathematics is upstream from much human progress, so I guess we should at least consider it. On the other hand, training in the punishing and mind-bending discipline of mathematics is IMO one of the highest achievements of the human race, not to mention one of the best ways we know of infusing our squishy meat brains, so losing the incentive to do it may do bad things to us. [TODO clarify]
I don’t know what to do about that.
8 Incoming
On how and why a sequence model reasons at all, not yet integrated:
- FranxYao/chain-of-thought-hub / Towards Complex Reasoning: the Polaris of Large Language Models (Fu et al. 2023)
- Unveiling Transformers with LEGO (Zhang et al. 2022)
- Neural algorithmic reasoning
- New methods boost reasoning in small and large language models — Microsoft Research
And:
- Resolution (fka Sequent): scale and automation for higher confidence in alignment — AI Alignment Forum
- Raschka (2026) — DIY reasoning models
- Improving Mathematical Reasoning with Process Supervision
- sanderwood/bgpt: Beyond Language Models: Byte Models are Digital World Simulators (Wu et al. 2024)
- videlalvaro/llm-arithmetic-internals: Mechanistic experiments on how LLMs represent and compute arithmetic internally, with strict no-parser controls, reproducible audits, and an interactive article.
9 References
Footnotes
Mac picks here, for the ones we can run at home.↩︎
What it costs to actually run one of these is in the build notes.↩︎
e.g. set \(T \approx 0.6\), \(k = 8\) to \(16\) and reseed↩︎
Mind the marketing on Aleph. Logical Intelligence frames it as a step beyond LLMs toward an energy-based reasoner that “does not think in words”, but by their own telling the benchmarked Aleph is built on an LLM, and the language-free model is a separate, unreleased, unbenchmarked thing.↩︎