Specter Labs

Wonton Soup

Lean proof searches rerun with one tactic blocked, mapping which routes to a theorem remain.

D-002status activeactivity 2026-10-23license Mixed

How does a prover’s set of moves shape the proofs it can find?

In this recorded search, the original run closes the theorem with trivial in one step, and with trivial blocked it reaches the same result through three algebraic steps.

Report · B-001

Proof search with a missing tactic

We block one tactic from a successful Lean proof search and rerun it under the same budget to see whether the prover still reaches the theorem by another route.

Inspect individual searches
encode(inl a) = 2 · encode(a)trivialOriginal routeringnorm_numringAlternate route

Proof found in 1 step

A recorded heuristic search in Lean. The theorem describes how a value tagged “left” is encoded as a natural number.
Inspect the recorded proof steps

encode_inl, same seed and search budget. As a control we also reran the search with decide blocked, a tactic it never had available, and it repeated the original route.

  1. ring rearranges the multiplication on the right.
  2. norm_num unfolds the encoding and simplifies the numbers.
  3. ring closes 2 · encode(a) = encode(a) · 2.
  • Report describes the search, the tactic blocks and the structural comparisons.
  • Dashboard opens individual theorem traces and run data.
  • Cabinet docs explain the lake and how to rerun things.