Research note · v0.1 · June 2026
Seven findings on joules per verified output.
The recipe for AI theorem proving is published. The open-weight implementations match the closed ones on the public benchmarks. The substrate — Lean, Mathlib, Z3, Coq, Isabelle, HOL Light — is open source. What is unevenly attacked is the energy cost. Seven findings from auditing the published record against the seven axes, closing on the Kepler step.
Finding 01
Inference search dominates the energy budget.
A coarse decomposition of where joules go in a modern autonomous prover: inference-time LLM forward passes during search — generating candidate tactics, exploring the proof tree, and burning whole generations on attempts that never compile — account for the overwhelming majority. The verifier (kernel re-checking, SMT discharge) is comparatively cheap; CPU-bound and deterministic, it adds up at scale but is not the bottleneck. Training is large but amortized across all proofs ever produced.
The implication is that joule reduction must be attacked on inference, not on the verifier and not on training. The escalation ladder is built on this fact: most subgoals do not need a learned model at all.
Finding 02
The S-axis distribution of real proofs is highly skewed.
In any reasonable proof corpus, a large fraction of subgoals close at S₁ (kernel automation) or S₂ (decision procedure) — the cheapest two tiers — provided the router is wired correctly. The waste mode in capability-maximalist systems is not that the lower tiers fail; it is that the system never tries them. A frontier model is invoked to discharge a goal that omega closes in microseconds.
Routing is therefore not an optimization. It is the architecture. The headline energy reduction available from routing alone — without any new training, new model, or new tactic — is large, immediate, and reportable. It is also the wedge that other systems cannot bolt on without rebuilding the inference loop they currently have.
Finding 03
Constrained decoding kills generate-then-fail-to-parse.
The dominant in-search waste, after wrong-tier placement, is the model emitting tokens that do not produce a well-formed Lean term — the proof attempt is rejected at parse, not at semantics. Grammar- and type-constrained decoding restricts emission to tokens that keep the partial proof legal. The constraint is a runtime mask over the logit distribution; no retraining is required.
The energy delta is measured at the generation step, not the verification step. The verifier was going to reject the attempt either way; the question is whether the joules to produce the rejected tokens were paid. With constraints they are not.
Finding 04
The lemma cache is an energy flywheel.
A proof that closes cold (no premise selection) pays full search cost. A proof that closes lemma-warm reuses the work that earlier proofs already paid for. The ratio is not subtle: a single applicable lemma can collapse a multi-step search into a one-line apply.
Premise selection over a curated library (Mathlib for math; project-local lemma graphs for code) compounds: every accepted proof becomes a premise candidate for every future search. The data flywheel becomes an energy flywheel. The C axis is what names this compounding.
Finding 05
The Amdahl tail dominates the headline.
Routing wins the easy eighty percent. On the genuinely hard goals, the frontier-model tier dominates the remaining energy — and the remaining energy is most of the total. A clean Pareto chart hides this; the headline "X joules per average proof" obscures the long tail. The honest report is the distribution, with the difficulty-axis (D) breakdown.
This is structural. It does not mean efficiency is uninteresting; it means efficiency is most defensible where the goal is to verify many tractable artifacts (most code, most engineering) and least defensible where the goal is to crack a small number of frontier problems.
Finding 06
The verifier is the attack surface, not the trust root.
A verifier-as-reward loop optimizes for "the kernel accepts it." Reinforcement-learning systems are documented to find exploits — small bugs in tactics, gaps between the spec and what the prover actually accepts, misformalized statements that flatter or distort results. Tao's working note on the matter is direct: RL is good at finding backdoors in proof assistants.
The mitigation is structural: the trusted core of the kernel must be kept small and audited; statements must be reviewed for misformalization before they are used as reward; and the proof artifact must be inspectable so that "verified" can be re-checked, not just believed.
Finding 07
The binding constraint on "verify everything" is the spec, not the prover.
A verified output of the wrong specification is worthless. Most application code has no formal specification — the prover cannot verify against a spec that does not exist. The addressable market for verified output is therefore the set of artifacts that already have, or can cheaply acquire, a formal spec: cryptographic primitives (HACL*, Fiat-Crypto), microkernels (seL4), compilers (CompCert), hardware (the EDA formal-verification tradition), and policy/compliance properties.
The frontier-prover wave is real and accelerating. But the dollar value of "verify all AI-generated code" is gated upstream of the prover. The honest framing is: cheap verification unlocks the slice of code where the spec already exists, and creates pressure to write specs where they did not. Not infinity.
The Kepler step
E(x) ≥ θ(D) · μ(S, V).
The joules to verify an output x are bounded below by a Landauer-class θ for difficulty D, multiplied by an impedance-mismatch μ between the solver tier S and the verifier kind V. Cheap solvers paired with their natural verifiers sit at the floor (kernel automation paired with the kernel — μ ≈ 1, θ at the substrate floor for D = trivial). Mismatch is multiplicative: a frontier model invoked to close a decidable arithmetic goal is twelve orders above the floor not because the goal is hard but because the solver was wrong for it.
This is the direct child of the relation on stack.openie.dev: E(x) = Σ θ(p) · μ(p, H). It is testable as the table fills with measured (E, S, V, D) tuples. Empties at well-attested intersections become predictions: pairings the stack permits but no system has yet built.