Proof search with a missing tactic

In one Wonton search, the prover found a proof using contrapose!, and when we blocked that tactic it still reached the theorem, this time through intro and exact. It is a small detour, but it gets at something we wanted to understand about proof search: if a theorem admits several proofs, how many of them can a particular prover actually reach when the route it normally takes becomes unavailable?

The difficulty is that even visibly different proofs can depend on the same tactic, so collecting more of them need not give the prover another way through. We record the attempted tactics and intermediate goals, remove a tactic from a successful search, and give the prover the same budget to try again, which lets us follow where the alternatives come from and where they run out. Some searches recover, some fail, and occasionally removing a move helps by taking an unproductive possibility out of the search.

Following the detour

At each unfinished goal, the prover proposes tactics and explores the proof states they produce, with each attempt either failing, opening further goals, or completing the proof. The examples below follow three successful searches through tactic removal so that we can see what changed along the way, including cases where the final success would otherwise make the intervention look inconsequential.

In the first example, blocking contraposition sends the prover through a direct argument in which it assumes the premise and derives the conclusion. The other two are more local substitutions: the sequence of goals stays similar, but a different final step closes the proof, so even a comparison of graph shapes would miss part of what happened.

The gallery records early examples from February 2026. Its graph distances describe changes in the recorded searches; repeated structures do not by themselves establish dynamical attractors.

The control changed too

Before attributing a changed proof to the tactic block, we needed to know how much the search could change when its available choices stayed the same. We repeated it with a tactic disabled that was already unavailable to the original run (an inert intervention), and although ReProver repeated consistently, some DeepSeek results changed under this control too.

We had fixed the search seed, but the model server was still sampling new tactic suggestions, and difficult theorems made more calls to that server, giving small differences more opportunities to redirect the search. Without the inert rerun, we could have mistaken those differences for an effect of the tactic we intended to study. A configuration flag named deterministic_inference made the problem easy to miss because it fixed only the search seed, and earlier DeepSeek campaigns had mostly run without the paired controls that would have exposed it.

The controlled comparison therefore requires both the original search and its inert rerun to solve the theorem before we ask what happens when a tactic used by the successful search is actually blocked.

When removing a move helps

Removing a tactic can help when it cuts off a branch on which the prover would otherwise spend its budget, leaving more attempts for a route that succeeds. In those cases the restricted search may reach a theorem the original search missed, or reach it sooner, and the trace lets us investigate that improvement by following where the attempts went. A restriction changes the allocation of a finite search as well as the set of moves available to it.

To compare that cost with a specified blind policy, we use $K = \log_{10}(\tau_{blind}/\tau_{agent})$, which expresses the saving in orders of magnitude when both policies face the same moves, constraints, goal, horizon, and cost units. These choices define the comparison, so changing them changes what the number tells us; the K reference works through them, while the analysis reference distinguishes the measurements stored by Wonton.

What can travel between systems?

One reason we became interested in this experiment is Levin’s TAME framework, and the question running through it of how a system reaches the same outcome when it has to find another way. Proof search gives us an unusually explicit version of that problem, because the goal is supplied in advance, a checker determines whether it has been reached, and the trace lets us inspect the attempts made under the new constraint.

With a developing body, we first have to decide which features of its organization count as persisting or recovering, which makes the comparison harder and also part of what we want to investigate. We can still ask which routes remain available after an intervention and what resources those routes share, using the Wonton result to motivate a more specific question: could the variety we observe among forms or behaviors also overstate their resilience when they depend on the same vulnerable mechanism?

For proofs, we can test this by grouping them according to the lemmas and tactic resources they use, then asking whether that description predicts survival on held-out theorem–prover groups better than counting proof shapes. That would give us a chance to explain why the diversity prediction failed, and to distinguish alternatives that merely look different from ones the prover can actually use when a resource disappears.

This article records the early experimental framework, and the counts from the later controlled tactic-blocking cohort are being re-audited before we publish them again. Selected runs are available in the Wonton Soup Dashboard.

The Cabinet documents search scheduling, backend differences, and the files needed to reproduce the comparisons.