# Proof embeddings — vector_behavior

Vectors for the proofs, made with the same models and the same pooling as the statement
spaces already in this repo, so the two are directly comparable.

| directory | what one row is | rows | dim |
|---|---|---|---|
| `proof_emb/e5-large-v2_theorem/` | one theorem's whole tactic script | 61,542 | 1024 |
| `proof_emb/e5-large-v2_step/` | one tactic invocation with its goal state | ~259,580 | 1024 |
| `proof_emb/e5-mistral-7b-instruct_theorem/` | one theorem's whole tactic script | 61,542 | 4096 |

Each directory holds `embeddings.npy`, `idx_to_name.json`, `meta.json`, and for the step
granularity `step_meta.json.gz` with the theorem, step index and premises per row.

## Lining a proof up with its statement

Row `i` of a proof space is the theorem named at `idx_to_name.json[i]`. The statement
spaces are keyed the same way, so going between them is a name lookup:

```python
import json, numpy as np

P  = np.load("proof_emb/e5-large-v2_theorem/embeddings.npy")
pn = json.load(open("proof_emb/e5-large-v2_theorem/idx_to_name.json"))
S  = np.load("embeddings/e5_large/embeddings.npy")
sn = json.load(open("embeddings/e5_large/idx_to_name.json"))

si = {n: i for i, n in enumerate(sn)}
both = [(i, si[n]) for i, n in enumerate(pn) if n in si]   # 56,467 theorems
pi, sj = zip(*both)
proof_vecs, stmt_vecs = P[list(pi)], S[list(sj)]
```

56,467 of the 61,542 proved theorems are also in the 99,552-theorem statement pool. The
rest have proofs but no statement embedding.

For step rows, `idx_to_name.json[i]` is `"<theorem>#<step index>"`; split on `#` to get
back to the theorem.

## Truncation

Proofs are much longer than statements and everything is encoded at 512 tokens, so long
tactic scripts are cut off. The exact count is in each directory's `meta.json` as
`n_truncated` / `frac_truncated` — check it before drawing conclusions about long proofs.

## Please read this before using them

In the parent study proofs are **held back on purpose**. Every claim about discovered
structure is checked by asking whether the grouped theorems share proof premises, and
that check has force only because no encoder was ever shown a proof.

These vectors break that. Any structure found with them cannot then be validated against
proofs — that is confirming a finding with the thing that produced it. Validate with
something else: human judgement, a held-out corpus, or the source organisation.

The same applies to `real_pairs_verified.json.gz` in this repo, which is the answer key
for the pairing step rather than the discovery step.