# Proofs — vector_behavior

Companion to the theorem/embedding bundle. Extracted from LeanDojo's traced tactics.

| file | contents |
|---|---|
| `proofs.json.gz` | `{theorem: [{tactic, premises}, ...]}` — the tactic script and the lemmas each step invokes |
| `proofs_full.json.gz` | the same, plus `state_before` / `state_after` per tactic |

```python
import gzip, json
proofs = json.load(gzip.open("proofs.json.gz", "rt"))

p = proofs["Finpartition.energy_le_one"]
for step in p:
    print(step["tactic"], "  uses:", step["premises"])
```

Theorem names match `results_shared/pool.json` and every `idx_to_name.json` in the
bundle, so a row index in an embedding array maps straight to its proof.

## Coverage

Not every theorem has a traced proof — many are proved by a single term or by
automation that leaves no tactic trace. Coverage figures are printed when this file is
generated and repeated at the bottom.

## Please read this before using them

In the parent study, proofs are **held back deliberately**. They are the answer key:
every claim about discovered structure is checked by asking whether the grouped pairs
share proof premises, and that check has force only because no encoder was ever shown a
proof.

If you use proofs to *find* structure, validate it with something else — human
judgement, a held-out corpus, or the source-file organisation. Finding a pattern with
proofs and confirming it with the same proofs proves nothing.

## Coverage in this export

- 61,542 theorems with a tactic proof, 259,580 tactic steps
- 56,467 of the 99,552 pool theorems (56.7%)