Seven orthogonal dimensions.

01 · WHAT PRODUCED THE STEP

placement on the escalation ladder

Solver tier

The mechanism that emitted the proof step. The ladder, cheapest first: kernel automation (built-in tactics that close decidable goals at CPU cost — simp, omega, ring, decide, aesop, polyrith); decision procedures (Z3, CVC5, Vampire) called from the kernel for the large decidable fragments; small distilled prover (in-domain 1–7B model, or MoE with few active parameters, with constrained decoding); frontier reasoning model invoked only at the leaves; hybrid tree-search where step generators and verifier feedback are looped under MCTS or best-first. Energy scales with active parameters multiplied by tokens emitted; cheapness is not subtle.

Admissible classes

Citations

Polu & Sutskever, arXiv 2009.03393 (2020) — GPT-f. · Polu et al., arXiv 2202.01344 (2022) — expert iteration. · Trinh et al., AlphaGeometry, Nature 625 (2024). · Lin et al., Goedel-Prover-V2, arXiv 2025.

02 · WHAT CHECKS THE ARTIFACT

the deterministic judge

Verifier kind

The non-LLM oracle that returns a clean binary pass/fail. The kernel-verifier class includes proof-assistant kernels (Lean, Coq/Rocq, Isabelle/HOL, HOL Light, Agda, Metamath, Mizar) whose small trusted core re-checks every step. SMT solvers (Z3, CVC5, Vampire, Yices) discharge first-order theories. Bounded model checkers (CBMC, Kani over CBMC) explore reachable state spaces up to a depth. The type system itself verifies a narrower class — Rust's borrow-checker proves memory safety and data-race freedom by construction. Runtime monitors enforce properties as side effects of execution. Hand audits remain the human-readable bound. The choice of verifier names what guarantee the artifact actually carries.

Admissible classes

Citations

de Moura & Ullrich, CADE 28 (2021) — Lean 4 kernel. · Barrett & Tinelli, Handbook of Model Checking (2018) — SMT. · Clarke et al., CBMC, TACAS (2004). · Jung et al., RustBelt, POPL (2018).

03 · JOULES PER VERIFIED OUTPUT

log₁₀ orders above Landauer floor

Energy class

Energy dissipated to verify one output, log-binned. The Landauer floor for a single bit-erasure is k_B T · ln 2 ≈ 2.87 × 10⁻²¹ J at room temperature. A verified output is many bits, but the structural point is that a kernel-automation closure operates within a small constant of the substrate floor while a frontier-model search burns ~10⁹–10¹² Landauer-equivalents per proof — twelve to fifteen orders of magnitude of head room, almost all of it inference search. The current published bound on serious autonomous proof attempts is several million tokens and hundreds of GPU-minutes per hard problem. This axis is the spine of the stack.

Admissible classes

Citations

Landauer, IBM J. Res. Dev. 5 (1961). · Bérut, Petrosyan, Ciliberto, Nature 483 (2012). · Niu et al., TokenPowerBench, AAAI 2026.

04 · WHAT THE GOAL IS

where the subgoal sits on the difficulty scale

Difficulty regime

The class of the goal being discharged. A trivial closure is a tactic-line collapse — type-checking, arithmetic over a small bounded fragment, a rewrite plus reflection. A decidable fragment falls inside the published soundness/completeness envelope of a decision procedure. An undergraduate-mathematics goal corresponds roughly to a curriculum-difficulty problem with a known solution path; competition mathematics (Olympiad, Putnam) pushes into combinatorial creativity within a finite library; research conjectures escape both fixed libraries and bounded search horizons. The axis matters because a single Pareto chart hides everything: hard goals are a long tail that dominate total cost, and Amdahl pressure on the cheap end limits the headline multiple.

Admissible classes

Citations

Zheng et al., miniF2F, ICLR (2022). · Tsoukalas et al., PutnamBench, NeurIPS D&B (2024). · Glazer et al., FrontierMath, arXiv 2411.04872 (2024).

05 · WHETHER THE WORK WAS DONE BEFORE

reuse class of the closure

Cache regime

How much of the work was already paid for. A cold proof starts with neither lemmas nor an applicable cached subproof, paying full search cost. A lemma-warm proof retrieves applicable lemmas from a curated library (Mathlib, stdlib, project-local) via premise selection — the dominant standing speedup in real proof engineering. A proof-hot regime serves the cached, verified subproof itself (memoization keyed on the goal's normal form). A distilled regime has compiled the result into model weights — the parameters carry the answer; no retrieval at all. Every successful proof feeds the next: the data flywheel becomes an energy flywheel.

Admissible classes

Citations

Irving et al., HOList & DeepHOL, NeurIPS (2018) — premise selection. · Yang et al., LeanDojo, NeurIPS D&B (2023) — retrieval-augmented proving. · Polu et al., arXiv 2202.01344 (2022) — expert iteration as distillation.

06 · WOULD THE SAME ATTEMPT YIELD THE SAME PROOF

determinism class of the producer

Reproducibility

The producer's determinism class. A deterministic solver returns the same proof bit-for-bit on the same input (Lean tactics with no randomization, SMT with a fixed seed, a quantized model with sampling temperature zero and KV-cache discipline). A seeded run is deterministic given the seed and is reproducible across machines that agree on numerics. A stochastic-bounded run is non-deterministic but with a published distribution over outcomes — pass@k figures live here. A stochastic-unbounded run depends on wall-clock racing, scheduling, or external services and is not meaningfully reproducible. Reproducibility is the precondition for audit; without it, "verified" is a single-roll claim, not a property.

Admissible classes

Citations

Goldwasser, Micali & Rackoff, SICOMP 18 (1989) — bounded probabilistic verification. · Aaronson, lectures on the polynomial hierarchy and pass@k (online). · McCullough & Vinge, Nature 506 (2014) — replicability in computational science.

07 · WHAT HAPPENS TO THE ARTIFACT

lifecycle after first verification

Persistence

What survives after the verifier returns pass. An ephemeral artifact is discarded on the next run — the search wrote, the kernel checked, and nothing was kept. A retained artifact is committed to a local proof database, available to the same project but not to others. An indexed artifact is normalized, deduplicated, and made searchable across projects (the OpenIE proof DB, shared lemma graphs). A library-integrated artifact has been promoted into a canonical library (Mathlib, stdlib equivalents) — visible to every downstream user, available for premise selection on the next cold proof. The axis names the rate at which today's joules subsidize tomorrow's.

Admissible classes

Citations

Buzzard et al., Mathlib4 in Lean 4 (2024). · Hales et al., Flyspeck Project — formalization of the Kepler Conjecture (2014).