SPECTER LABS

Wonton Soup

Lean proof searches rerun with one tactic removed, testing which routes to a theorem remain available.

D-002status activeactivity 2026-10-16license Mixedscope expansion

Removing a tactic can lead to a different proof

The tactic trivial closes this theorem in one step. With that tactic disabled, the search reaches the same result through three algebraic steps. The unchanged control repeats the original route.

Read the articleInspect 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. The unchanged control blocks decide, which was already unavailable in the original search.

  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.
  • Article 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.