Abstract proof concepts in a frozen prover.

Headline findings

Five findings.

1. Abstract proof concepts are readable off the frozen prover, with no training. Math domain classifies at 0.95 (6 classes, chance 0.167); tactic from the statement at 0.73 (5 classes, chance 0.20). Both sit far above the surface literal baseline (0.79 and 0.54) and a shuffled-label control at chance.
2. On statement properties the prover has only a small edge over a general encoder; on the tactic decision it has a large one. Domain: prover 0.950 against 0.908. Tactic read from the statement: 0.729 against 0.679 — but that is the wrong probe. Read at the mid-proof decision state, the prover predicts its next tactic at 0.867 against 0.643 for a general encoder of the same proof-so-far, an edge of +0.224.
3. Concepts sit at modestly different depths, with different shapes. Domain peaks sharply at layer 10 (0.950) and declines to 0.796 by layer 35. Tactic peaks at layer 14 (0.741) as a broad plateau, 0.70–0.74 across layers 12–20. Proof structure is read a little deeper than topic and is more diffuse over depth.
4. The representation is a graded continuum, not a hard partition. Same-class rank-fraction is about 0.40–0.43 against a chance of 0.5: local and graded. Classify with a global whitened head and retrieve by graded nearest neighbours; do not carve a partition.
5. Distributed, not localized. Domain reads at about 0.93–0.95 across attention, MLP, gate and activated-gate sites at the early-mid block. There is no single magic site.

The central result

Goal versus decision.

Teacher-force each winning Lean proof. At each tactic line, capture the activation at the position that predicts the tactic token — the state before it is emitted, when the model has not yet seen the tactic. That gives 750 balanced decision points across five tactics (apply, rw, exact, simp, intro) from 351 proofs, read at the activated-gate site.

Decision-state accuracy by layer: 0.829 at layer 8, 0.825 at 10, 0.839 at 12, 0.833 at 14, 0.848 at 16, and 0.867 at 20 — rising with depth, while the graded rank-fraction tightens from 0.38 to 0.31. The control stays at 0.21. Layers 24–35 were deliberately not probed, to stay out of the near-tautological regime next to the output head.

A model beating a text encoder at predicting its own next tactic is partly expected, because the model is what generates it. The interpretability content is that the decision is linear and mid-network, +0.224 above the surface. See it drawn, with the raw activations →

Statement properties

The dissociation table, with one consistent baseline.

Robustness: domain reads 0.950 on seed 0 and 0.929 on a fresh sample (seed 1), a difference of 0.021. Against the QED corpus's own specialised embedding the prover is at parity on domain (0.950 against 0.961).

Depth map

Leakage-free whitened accuracy by layer at the activated-gate site.

Most readable cells for domain

An earlier gap between MLP output (0.858) and attention output (0.929) was sample size — 360 against 480 prompts — not site. With matched data they tie. The fast nearest-centroid grid also mis-ranks cells; it is used only to shortlist, and the whitened head is the readout.

Corrections

Two headlines that did not survive.

Both were published inside this line of work and then withdrawn. They stay in the report because a process that only shows its wins cannot be audited.

Causal check

One direction steers the choice.

Adding a single mass-mean direction to the residual stream at layer 16, at one position, with the dose scaled to the norm of the hidden state. Δp is the mean change in the model's own next-token probability for the target; "flip" is the share of lines whose top token becomes the target. 60 proofs, 285 decision lines, 101 steered lines. Nulls are three equal-energy directions (random, shuffled, orthogonal) at dose 2.

The direction causally steers exact, simp and have well above the nulls, with an inverted-U dose response: past the ceiling the top token degenerates and the model loses the plot. It does not steer apply or rw — the lemma-name family the whitened reading also confuses (apply↔exact 28, rw↔apply 30, simp↔rw 21 of 750). "Next comes a lemma name" appears to be shared between them. Every steered line is on the proof reader →

The proofs

57 recognisable theorems, all proved by the model.

The proof reader shows only proofs the prover wrote and Lean compiled. 47 were selected from the solved ledger for being recognisable: Wilson's theorem, the freshman's dream in ZMod p, Euclid's lemma, Gauss's Σ φ(d) = n, the triangle inequality, the geometric series, the chain rule, Hahn–Banach, and others.

Classics missing from the ledger were then attempted directly: 22 statements in Lean 4 with Mathlib, several heads per target, each head certified by compiling it and checking that its axioms do not include sorryAx.

Certified: √2 is not a ratio of integers, both De Morgan laws, the contrapositive, Cauchy–Schwarz in two dimensions, AM–GM in squared form, Fermat's little theorem, gcd·lcm = a·b, the pigeonhole principle, and |𝒫(s)| = 2ⁿ — all multi-step, 5 to 22 tactic lines.

Still missing, and reported as such: √2 irrational in statement form, both infinitude-of-primes forms, the Gauss sums, the sum of odd numbers, the geometric sum, AM–GM with a square root, the triangle inequality for |·|, Bernoulli's inequality, the binomial theorem, and "n² even implies n even". These are real prover misses at this sampling budget, not pipeline failures. Retrieval plus six heads lifted the rate from 12% to 71%.