Proofs Compound. Pattern Matching Doesn’t.

Scaling improves pattern matching, and the AI industry has organized around scale as the path to capability. What scale produces and what compounds are not the same thing. A system that keeps the proofs it produces can measure its own compounding: the share of new work that extends prior verified work instead of starting from scratch.

AlphaGeometry showed what verification can do in 2024. A symbolic deduction engine, working from random premises, generated 100 million synthetic geometry theorems and proofs. Every one was correct by construction, because the engine derives each step from the rules of geometry. A language model trained on those proofs learned to propose the extra constructions, such as a new point or line, that the engine needed to get unstuck. The system solved 25 of 30 olympiad geometry problems, close to the 25.9 an average International Mathematical Olympiad gold medalist solves. GPT-4 solved none (Trinh et al. 2024). Its successor surpassed the average gold medalist the following year (Chervonyi et al. 2025).

The training data came from a rule-based engine rather than human preference. That is a different source of signal, and it produces a different kind of system.

Scaling a pretrained model makes its guesses better. A system that keeps its proofs accumulates something pretraining cannot produce: a corpus of validated reasoning that grows every time the system runs. The corpus is queryable, citable, and extensible. Weights are none of those things.

What scale improves

Scale does real work. Fluency, recall, format adherence, and translation quality have all improved substantially as models have grown. These gains are visible in any deployed system. They are also concentrated on a specific axis: the quality of the pattern match between input context and trained-on output. Scale improves the match.

Scale does not improve verification. A larger model produces more fluent guesses. It cannot produce guesses that have been checked against anything other than the training distribution. A pretrained model at any size is a pattern matcher, and the thing it is matching is the shape of text that was statistically common in training. Closeness to that shape is what scaling optimizes. Correctness is a different property.

Verification as the training signal

Reinforcement Learning from Human Feedback (RLHF) was the industry’s first main attempt to close this gap. Human raters compare candidate outputs and mark the better one. A reward model learns to predict the human preferences. The language model is fine-tuned against the reward model. The outputs are agreeable and polished. Correctness is incidental. The reward model is a proxy for correctness when the human rater can evaluate the answer. When the answer is beyond the rater’s domain, the proxy breaks. The fine-tuning continues, optimizing toward something else.

The industry has since moved toward the verifier. Reasoning models trained with reinforcement learning against checkable rewards, where an answer is compared with a known result or code is run against tests, became the main route to better reasoning in 2025. DeepSeek-R1 published the method in detail (DeepSeek-AI 2025). AlphaProof applied the same idea to formal mathematics, learning from proofs the Lean proof assistant accepted. Combined with AlphaGeometry 2, the system reached silver-medal standard at the 2024 International Mathematical Olympiad (Hubert et al. 2025).

Verifier-based training inverts the RLHF structure. The training signal comes from verifier acceptance rather than human approval. The verifier is architecturally separate from the generator and may not even be a language model. It can be a symbolic engine, a theorem prover, a unit test, a type checker, or a combination of these. It evaluates candidate reasoning against a rule independent of the generator.

A proof, in this sense, is a recorded chain of reasoning together with the check it passed. The checks differ in strength. A formal proof settles a claim. Passing tests shows that the tested cases work.

RLHF learns what labelers like. Verifier-based training learns what the check accepts. When a labeler cannot evaluate an answer, RLHF optimizes toward the appearance of correctness. A verifier rewards whatever passes the check, so it is only as good as its specification: a model trained against weak tests can learn to pass them without solving the problem. Against a strong specification, appearance earns nothing.

The difference in behavior shows up when the verifier also runs while the system is in use. A system that checks its output before releasing it either produces verified output or surfaces the gap explicitly. A system that met a verifier only in training produces fluent output at the edge of its knowledge, like any other model.

The separation matters because capability and constraint entangle when they share weights. A single model trained to both generate and judge its own outputs faces a mechanical problem. Gradient updates toward better generation shift the judging distribution. Updates toward stricter judging shift the generating distribution. Separating the roles into distinct components keeps the verifier independent of generator drift.

Where specifications exist

AlphaGeometry worked in formal geometry because geometric correctness has a formal definition. The pattern is not restricted to geometry. Code that passes its tests, schemas that validate against their definitions, mathematical proofs that close in a proof assistant, logical derivations that satisfy their inference rules: each is a specification a verifier can check against.

The bottleneck for verifier-based training is the availability of specifications, not scale. Many domains already have them in executable form: test suites, schemas, type systems, and proof assistants. In much other knowledge work, review plays the same role. Work product is reviewed, corrected, and iterated against criteria that are real but often unwritten. Those criteria become usable by a verifier only once someone writes them down as checks, and that work is the practical limit on how far the approach reaches.

Keep the proofs

Most training pipelines produce one artifact: an updated model. A generator-verifier system produces two. Weights update as usual. The verifier’s acceptance record is itself an artifact, separate from the weights and persisting beyond the training step.

Most generator-verifier systems, including the reasoning models trained against verifiers, use the proof as a training signal and discard it. The proof contains something the weights cannot: the explicit chain of reasoning that was validated, the premises it rested on, and the specification it was checked against.

The discard is the mistake.

A proof that is kept becomes part of a corpus. The corpus grows every time the system produces a validated proof. It shrinks only when a proof is retracted, which happens when a premise it depended on is invalidated. Between retractions, the corpus grows monotonically. Every query is against the accumulated total, not the latest training batch.

The corpus is structured. Proofs are indexed by their conclusions, their premises, the specifications they were checked against, and the domain they address. A new claim can be looked up against the corpus to find prior proofs whose conclusions overlap with it. A premise set surfaces proofs that used those premises. The system’s verified reasoning is addressable.

When a new claim arrives, the generator’s first step is to check the corpus. If a prior proof covers the claim or overlaps closely, the work collapses from generation to citation. The generator extends the prior proof rather than deriving a new one from scratch. Extension is faster than derivation. It is also structurally safer, because the extension builds on a base that has already passed verification.

Weights are opaque and recomputed on every major training run. A corpus persists. It can be audited, inspected, versioned, and shared across deployments. When a system is updated or replaced, the corpus transfers.

The accumulated reasoning survives the model that generated it.

The compounding signature

A new deployment of a proof-based system has an empty corpus. Every claim requires derivation. There are no prior proofs to extend, and the generator works from scratch every time. Over time, the corpus fills. New claims increasingly overlap with prior proofs. The generator’s first check succeeds more often, and work collapses from derivation to extension. The ratio of extend-to-derive rises as the corpus grows. This ratio is the compounding signature.

The ratio is observable. Every proof logged is either a derivation or an extension. Counting them is trivial. The ratio over time is a plot anyone with access to the corpus can produce.

This is the property that matters. Most claims about AI capability are claims about what the weights have learned. The weights are opaque. A benchmark score shows improvement on that benchmark without revealing what general capability was built. A corpus ratio is different: it counts how much of new work rests on validated prior work. The accumulation is directly visible.

Two further signatures develop alongside the primary one:

• Time-to-competence in a covered domain. A new task in a domain where the corpus has depth requires less derivation than the first task did. The generator finds prior proofs to extend, the verifier has precedent to compare against, and the new proof adds to what was already there. Time-to-competence falls as the corpus grows.
• Marginal cost of verified output. Derivation is expensive. It requires the generator to build a reasoning chain, the verifier to check every step, and retries when the chain fails validation. Extension is cheaper. A retrieved prior proof provides most of the chain, and only the new step needs verification. As the extend-to-derive ratio rises, the cost per validated output falls.

The rates at which these signatures develop in practice are not settled, and published curves do not yet exist. The structure follows from the architecture: in any system that retains proofs and keeps receiving work that overlaps what it has already proved, the signatures appear. The open question is how steep the curves are and how fast they settle. The ratios are there to be measured.

Why the corpus cannot be copied

Pretraining improves pattern matching. It does not produce verified reasoning or a proof corpus. Verifier-based post-training improves reasoning and then discards the proofs that did it.

Where a symbolic engine can manufacture proofs, anyone can manufacture them. AlphaGeometry’s training data came from its own deduction engine, and a competitor with a comparable engine can generate the same kind of data. Most domains have no such engine. Their proofs exist only where a system has been running against real work, checking its output, and keeping what passed. A competitor starting in such a domain cannot match a system that has been accumulating proofs there for a year.

Getting those proofs requires running the system. Running the system requires the architecture: generator, verifier, corpus, retrieval, the whole pipeline operating against a domain where specifications exist. The architecture can be rebuilt. The accumulation cannot. The corpus is a dataset that can be obtained only one way: by running a particular kind of system against a particular kind of problem over time.

The asymmetry compounds on itself. A system with a large corpus extends faster and produces verified output at lower cost. Its deployments operate cheaply, which means more deployments, which means more proofs, which means a larger corpus. A system without a corpus has to derive everything, pays full cost on each output, and competes at a structural disadvantage. The gap widens with every proof added.

A competitor can buy bigger models. A competitor can hire better researchers. A competitor cannot buy the accumulated proof corpus of a deployed proof-based system, because the corpus exists nowhere except in the system that produced it.

What survives the next model

Every AI system either accumulates verified work between training runs or it does not. Most do not. Deployment data may feed the next training run, but when a model is replaced, nothing it verified survives in a form the new model can cite. The next model starts from whatever its training gave it.

A proof-based system is different. The corpus survives the model. When a new model takes over, the accumulated reasoning is already there, indexed and available for extension. Capability persists across model replacement because it lives outside the weights.

The question for any AI capability program is what survives the next model replacement.

If the answer is the weights, the program is renting capability from a pretraining pipeline. If the answer is a corpus, the program is building capability that compounds.

References

• Chervonyi, Y., et al. (2025). Gold-medalist performance in solving olympiad geometry with AlphaGeometry2. arXiv:2502.03544.
• DeepSeek-AI (2025). DeepSeek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning. arXiv:2501.12948.
• Hubert, T., Mehta, R., Sartran, L., et al. (2025). Olympiad-level formal mathematical reasoning with reinforcement learning. Nature.
• Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024). Solving olympiad geometry without human demonstrations. Nature 625, 476–482.

Originally published on Medium.