Sekos keys 1 · 2 · 3
PYTHAGORAS-4B · PROOF READER
Lean theorem prover · frozen activations · read at the moment of decision

What the prover is about to do,
read off its activations — line by line.

Pick a proof the model wrote. At every tactic line, you see what it was about to do in its own words at each depth of the network, when it committed, what in the context it was looking at — and what happens when you push it toward a different tactic.

The strip = the model's own guess, depth by depth36 cells, early → late. Each is the next token the model would emit if stopped at that depth; outlined cells already say the tactic it finally chose. The marker is where it commits.
The tint = what the decision looked atClick a line: the proof text tints by the attention that decision paid each token — or switch to the concept direction to see where the tactic's signal lives.
Steer = push it, with controlsAdd a tactic direction to the residual stream at that one position and read the next token again. Three equal-energy random directions are the null.
proof 

    

  

  






  
Across all 750 decisions
How sure, and confused with what

  
The whitened readout on every captured decision state (layer 20). Each box is one real decision: its height is how much probability the reading gave the tactic the model actually chose; solid = read correctly, hollow = confused. The confusions are not noise — the classes blur along a hierarchy of what comes next.

  

    
Confidence, per decision

      

      
Squares-style columns (Ren et al.): read a column top-down — where the hollow boxes sit is where the reading fails. intro is almost never confused; apply and rw carry the long tails.

    
Which tactics blur together

      

  

  

    
When the reading is confident (existing captures)

      
First probed layer at which the whitened reading gives the chosen tactic p > 0.8. Three quarters of decisions are already readable at the earliest probed layer (L8); the later commits are the ambiguous apply / rw / simp lines. That is why depth is shown per line, not as a slider.

    
Controls worth knowing

      
Could you guess the tactic from the statement alone? Reading the theorem statement instead of the decision state gives 0.729 — and a general text encoder gets 0.679 on the same text. The prover's edge (0.867 vs 0.643) appears only at the decision state. That statement-only reading is a control, not a concept.

      
Domains. The math-domain reading (6 classes, 0.95 at layer 10) pairs Calculus↔Geometry and Logic↔Number Theory, with Algebra the hub everything is mistaken for. Its per-token paint over the statement ships once the domain set is re-captured with its statements logged.

      
Steering, across 101 steered lines (L16, 2× the residual norm). The tactic direction flips the model's own next token to exact on 99% of lines (mean Δp +0.74; nulls 16–18%), to simp on 61% (+0.34; 75% at 3×; nulls 18–19%), to have on 58% (+0.32; nulls 24–31%). It barely moves apply (7%) or rw (8%) — the lemma-name family the reading also blurs — so the mass-mean direction is not the whole story there. Past the ceiling the next token stops being a tactic; that is shown, not hidden.