Frontier search is the escape hatch.

Tactics shipped with the proof assistant: simp (rewriting), omega (linear arithmetic over integers), ring (commutative-ring normalization), decide (decidable propositions by reflection), aesop (hammer-style search over Lean lemmas), polyrith (polynomial arithmetic). CPU-bound, no GPU, often sub-second. A surprising fraction of subgoals in any real proof close here. Capability-maximalist labs spend GPU on what aesop discharges instantly; the ladder never does.

Z3, CVC5, Vampire, or Yices invoked from the kernel through a tactic interface. Discharges first-order theories with quantifiers, arrays, bit-vectors, linear and non-linear arithmetic — large decidable fragments at polynomial-to-exponential CPU cost. Orders of magnitude cheaper than tree search over LLM tokens for everything inside its envelope. The kernel re-checks the certificate; the SMT solver is a one-step oracle, not a trust root.

A 1–7B model trained for tactic prediction inside the chosen prover, or an MoE with few active parameters per token. Grammar-constrained decoding restricts emission to tokens that keep the Lean term well-formed — kills the dominant waste of generate-then-fail-to-parse. The model proposes a tactic; the kernel applies and checks; only verified steps are kept. Active parameters multiplied by tokens emitted is the energy bound, so a 7B at fifty tokens beats a 671B at five.

A large reasoning model invoked only at the leaves the lower tiers cannot reach: high-level strategy, the genuinely-novel lemma, the bridge step. Long chain-of-thought reasoning is expensive per token and per call; the ladder reserves it for goals where cheaper tiers have provably failed. Whole-proof drafts get repaired locally on tactic failure (proof repair, not regeneration) — the most common waste mode in autonomous attempts.

Best-first or MCTS over a proof tree, mixing the lower-tier solvers as step generators with verifier feedback as the reward signal. KV-cache sharing across sibling branches reuses the proof-state prefix instead of recomputing it — a search-specific serving optimization. The most expensive retrieval method by twelve orders of magnitude. Should be the last resort, not the default. Frontier and contest goals live here; nothing else should.