# Open Lean-prover teachers for distillation data (lane T2, 2026-10-19)

Goal: verified proofs from stronger open provers as one more SFT source for the Apache-2.0 research model (base:
Goedel-Prover-V2-8B). Nothing here touched a GPU. All sizes/licenses are from the HF hub API and model cards read on
2026-10-19; every miniF2F number is the AUTHORS' number under their own verifier, token cap and sampling, so none is comparable
to what we measure until reproduced in our harness (plan section 1).

## 1. Survey

| model | license (hub) | bf16 size | arch / Lean | reported miniF2F-test | verdict |
|---|---|---|---|---|---|
| **Goedel-LM/Goedel-Prover-V2-32B** | Apache-2.0 | 65.5 GB, 14 shards | Qwen3 dense, 64 L, 8 KV heads, ctx 40,960; Lean 4 + Mathlib, same stack as the 8B | 88.0% pass@32 (90.4% with self-correction); PutnamBench 43 @32 (57 with self-corr., 86 @192) | **best fitting teacher; downloaded** |
| deepseek-ai/DeepSeek-Prover-V2-7B | repo `LICENSE` is MIT (code), model card says **DeepSeek Model License** (use-based restrictions, see 1.1) | 13.8 GB | Llama, 30 L, **32 KV heads (MHA)**, YaRN x16 to 65,536 (card: 32K) | not on the card (7B row is in the paper, arXiv 2504.21801; not re-read here, so unverified); 671B: 88.9% | downloaded; **training use blocked on license (1.1)** |
| AI-MO/Kimina-Prover-72B | MIT | 145.4 GB | Qwen2, 80 L, 8 KV heads, ctx 131k | 84.0% pass@32 | does not fit bf16; no open AWQ/GPTQ safetensors (only GGUF); weaker than Goedel-32B; skip |
| AI-MO/Kimina-Prover-Distill-8B (= `Kimina-Prover-8B`, same sha) | Apache-2.0 | 16.4 GB | Qwen3-8B | 77.86% pass@32 | already on disk (docs/KIMINA_BASE.md); same size and weaker than our base, not a teacher |
| Kimina-Prover-Distill-1.7B / 0.6B, Preview-Distill-7B / 1.5B | Apache-2.0 | 4.1 / 1.5 / 15.2 / 3.6 GB | Qwen3 / Qwen2.5-Math | below the 8B | too weak to teach an 8B |
| stepfun-ai/StepFun-Prover-Preview-32B / 7B | Apache-2.0 | 65.5 / 15.2 GB | Qwen2 (R1-distill base) | 70.0% pass@1 (32B) | multi-turn REPL loop (`<sketch>`/`<REPL>`), not whole-proof; incompatible with `lean_gen`; skip |
| ByteDance-Seed/BFS-Prover-V2-7B / 32B | Apache-2.0 | 15.2 / 131.1 GB | Qwen2.5 | n/a here | next-tactic model for tree search, no whole-proof output; skip |
| ByteDance-Seed/Seed-Prover | not open (hub 401; paper/API only) | - | - | - | unavailable |
| mistralai/Leanstral-1.5-119B-A6B (and -2603) | Apache-2.0 | 120.9 GB | Mistral Small 4 MoE (119B total, ~6B active), agentic, ctx 256k | not read | does not fit bf16 on 92 GB; only NVFP4/GGUF/MLX community quants (Blackwell/Apple formats, untested on Ampere); agentic tool protocol, not whole-proof; separate lane |
| deepseek-ai/DeepSeek-Prover-V2-671B | DeepSeek Model License | 688.6 GB | - | 88.9% | out of reach |
| Goedel-LM/Goedel-Prover-SFT | MIT | 13.8 GB | DeepSeek-Prover-V1.5 base | ~57% | weaker than our base |

Quantised open variants found by hub search (names containing awq/gptq/fp8/bnb/nvfp4): Goedel-V2-32B: only
`mlx-community/...-8bit` (Apple); DeepSeek-Prover-V2-7B: `athanor-ai/...-GPTQ-4bit`, `unsloth/...-bnb-4bit`, `NVFP4/...-FP4`;
Kimina-72B and Kimina-8B: none. None is needed: the two models we use fit in bf16 (section 2). Third-party quantised copies are
not trusted as teachers anyway (unknown calibration, no license chain).

### 1.1 License finding (read before any DeepSeek output enters training)

The DeepSeek Model License (LICENSE-MODEL, the one the Prover-V2 card links) defines "Derivatives of the Model" to include "any
other model which is created ... by transfer of patterns of the ... output of the Model ... including distillation methods ...
or methods based on the generation of synthetic data by the Model for training the other model". Section 4 requires every
derivative to carry the Attachment-A use-based restrictions as an enforceable term. An SFT model trained on DeepSeek-Prover-V2
proofs is therefore a Derivative that cannot be released under plain Apache-2.0. The hub repo's `LICENSE` file is MIT, which
contradicts the card; the card + LICENSE-MODEL is the safer reading. **Decision for the owner**: either (a) do not train on
DeepSeek-Prover-V2 outputs (default here), or (b) accept Attachment-A on the released weights. Using it for evaluation or
as a baseline is unaffected. Goedel-V2-32B (Apache-2.0) and Kimina (MIT / Apache-2.0) carry no such clause. Apache-2.0 / MIT
model cards do not mention an output-use clause; we record the hub license string and card revision per teacher anyway.

## 2. Feasibility on 4x A10G (22.5 GiB usable each, 90 GiB total, TP=4, PCIe + host-SHM NCCL)

Model: per-GPU weights = bytes/4; KV bytes/token (global) = layers x 2 x kv_heads x head_dim x 2; each GPU stores 1/4 of the
heads. Per decode step each GPU reads its weight shard plus the live KV; step time = bytes / (eff x 600 GB/s). `eff` is
calibrated on OUR 8B measurement: 256 seqs at cap 16k = 1,363 tok/s (docs/P2.md, P2-B), mean completion 4,996 tokens, mean live
context about 5,000 gives eff = 0.46 (this folds in the NCCL cost). The model reproduces the 8B at 84 seqs as 1,171 tok/s
(measured 1,043 end-to-end / 1,015 in the smoke). Overhead reserved per GPU: 2.0 GiB (CUDA context, activations, graphs, NCCL).
These are ESTIMATES; the section 6 smoke replaces them.

| | Goedel-8B (ours, measured) | Goedel-V2-32B bf16 | same, util 0.94 | same, fp8 KV (untested on A10G) | DeepSeek-Prover-V2-7B bf16 | same, fp8 KV |
|---|---|---|---|---|---|---|
| weights / GPU | 3.8 GiB | **15.3 GiB** | 15.3 | 15.3 | 3.2 GiB | 3.2 |
| KV bytes / token (global) | 144 KiB | 256 KiB | 256 | 128 | **480 KiB (MHA)** | 240 |
| KV room / GPU at util 0.90 | 14.4 GiB | **3.0 GiB** | 3.9 (0.94) | 3.0 | 15.0 GiB | 15.0 |
| KV capacity (tokens) | 420k | **49k** | 64k | 98k | 131k | 263k |
| sequences at 16k / 32k (worst case) | 25 / 13 | **3.0 / 1.5** | 3.9 / 1.9 | 6 / 3 | 8 / 4 | 16 / 8 |
| sequences at mean live ctx 5k | 84 | **9** | 12 | 19 | 26 | 52 |
| est. tok/s | 1,000-1,360 | **~130** | ~160 | ~270 | ~365 | ~730 |
| `max_model_len` it can start with | 40,960 | 40,960 needs 2.5 GiB/GPU for one sequence: starts at 0.90, no headroom; use <= 33,000 | | | 32,768 | |

Reading: bf16 weights of the 32B fit (61 GiB of 90) but leave only ~3-4 GiB per GPU for KV, so the engine runs ~9-12
concurrent sequences, is KV-capacity-bound and runs at roughly **130-160 tok/s, 7-8x slower than the 8B**. It is the only
open model above our base that fits at all. The 7B teacher is not fast either: it is MHA (32 KV heads, 3.3x the KV per token of
Qwen3-8B), so its KV room, not its weights, caps it at ~365 tok/s. Alternatives considered: TP=2 x 2 replicas for the 7B gives the
same total capacity and doubles the engine count (no throughput gain, more load time); a 4-bit 32B (~18 GB) would free ~10 GiB
of KV per GPU and ~4x the concurrency, but no trustworthy open GPTQ/AWQ of Goedel-V2-32B exists and making one needs a
calibration run and 65 GB scratch we do not have headroom for: **not pursued**. The cheapest lever is `--kv-cache-dtype fp8` in
vLLM (2x capacity); on Ampere it is storage-only fp8 with a slower attention path, so measure it in the smoke before trusting the
~270 tok/s. Prefix caching (already on) helps nothing here: prompts are short and unique.

## 3. What was downloaded

All via `scripts/teachers/download_teacher.py` (disk floor 60 GB enforced against hub-reported bytes BEFORE fetching; 2 workers,
`nice -n 10 ionice -c3`, hostguard cap 2 cores / 8 GB, `HF_HUB_DISABLE_XET=1`), into `HF_HOME=/apps/development/rlhf/hf_cache`.

| repo | revision | path | size | check |
|---|---|---|---|---|
| deepseek-ai/DeepSeek-Prover-V2-7B | `a8d9e14432b2e8dd9df2a4d4e70f1ba9bc8d9b7b` | `hub/models--deepseek-ai--DeepSeek-Prover-V2-7B/snapshots/a8d9e144...` | 13.8 GB, 2 bf16 shards | `check_snapshot.py`: 273/273 tensors, shapes match, shards complete, 273 x BF16 |
| Goedel-LM/Goedel-Prover-V2-32B | `851bf85d329b0f819e1a44db30e05d16e07d15c0` | `hub/models--Goedel-LM--Goedel-Prover-V2-32B/snapshots/851bf85d...` | 65.5 GB | `check_snapshot.py`: 14/14 shards complete, 707/707 tensors present exactly once, every shape matches, 707 x BF16, all 25 files byte-size equal to the hub's; **warning: the upstream `model.safetensors.index.json` assigns 657 of 707 tensors to the wrong shard** (3.2) |

Disk: 148 GB free before the 32B (166 GB at the start of the lane), **74 GB free after** both (floor 60 GB; the disk is shared and other writers took ~10-15 GB during the 90 minutes, so re-check `df -h /apps` before any further download). Both downloads resumed cleanly after one `ReadTimeout`; no `.incomplete` blobs remain.

### 3.1 Verification tools

* `scripts/teachers/check_snapshot.py SNAPSHOT [--json]` (new, stdlib only, header-only, tested in
  `tests/test_teacher_check_snapshot.py`): config architecture (Llama / Qwen2 / Qwen3 dense), index key set equals the key set the
  config implies, every shard exists, header extents equal the file size (truncation), tensor-in-index-shard, every shape,
  dtypes. It reports `rope_scaling` / `sliding_window` / `tie_word_embeddings` rather than refusing.
* `scripts/p2/check_qwen3_snapshot.py` for the Qwen3-family 32B as well (it additionally proves the key set maps into
  `align`'s loader). `align` does not need to LOAD the 32B (teacher use is vLLM generation only); the check is for completeness.

### 3.2 Findings on the 32B snapshot

* **Upstream index defect.** All 707 tensors exist exactly once across the 14 shards and every shard header matches its file size,
  but `model.safetensors.index.json` (byte-identical to the hub's at this revision) names the wrong shard for 657 of them
  (e.g. `model.embed_tokens.weight` is in shard 1, the index says shard 3). vLLM and transformers read every shard listed in
  `weight_map` and are unaffected; `scripts/p2/check_qwen3_snapshot.py` reports NOT COMPATIBLE because `align`'s loader keys on
  the index. Consequence: use the 32B ONLY through vLLM (as planned); if `align` ever needs to load it, regenerate the index from the
  shard headers (a 20-line script, no weight I/O) rather than patching the snapshot in place. `check_snapshot.py --strict-index`
  turns the mismatch into a failure.
* Config: Qwen3ForCausalLM, 64 layers, hidden 5120, ffn 25600, 64 Q / 8 KV heads, head_dim 128, vocab 151,936, rope_theta 1e6, no rope
  scaling, max_position_embeddings 40,960, bf16, untied head.
* Tokenizer: `tokenizer.json`, `vocab.json`, `merges.txt`, `added_tokens.json`, `special_tokens_map.json`, `tokenizer_config.json` (so
  the chat template) are **byte-identical to Goedel-8B's**: token ids and the prompt render are unchanged.
* `generation_config.json` differs: 32B has only `eos_token_id 151645`, no sampling defaults; the 8B has temperature 0.6, top_k 20,
  top_p 0.95 and EOS `[151645, 151643]`. `lean_gen` passes temperature/top_p explicitly, but not top_k: do not let vLLM's
  `generation_config="auto"` supply different defaults per model (pass `--generation-config vllm`, or set top_k explicitly) so 8B and
  32B samples come from the same sampler.


## 4. Prompt formats (record of what each teacher expects)

| | Goedel-Prover-V2-32B | DeepSeek-Prover-V2-7B |
|---|---|---|
| chat template | stock Qwen3 (`<|im_start|>`), no BOS, EOS `<|im_end|>`; tokenizer and template byte-identical to the 8B's (3.2) | DeepSeek-V3 style: text starts with `bos_token` (`<｜begin▁of▁sentence｜>`, id 100000) + system, then `<｜User｜>{user}<｜Assistant｜>`; `add_bos_token = true`; EOS `<｜end▁of▁sentence｜>` (100001) |
| user prompt | the Goedel prompt, byte-identical to the 8B: `Complete the following Lean 4 code:\n\n```lean4\n{stmt}```\n\nBefore producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.\nThe plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.` | the same CoT prompt text, but the card's fence is `{stmt}\n```` (a newline before the closing fence); Goedel's is `{stmt}```` with none. The two are therefore NOT byte-identical: `goedel` format on DeepSeek is a one-newline deviation from the card, to be pinned and recorded (or add a `deepseek` format that inserts the newline; prefer that, 5 lines) |
| statement shown | `GOEDEL_HEADER` + `...:= by sorry` | card example: `import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n` + optional `/-- informal -/` docstring + theorem `:= by\n  sorry` (same header as `GOEDEL_HEADER`) |
| output | plan prose, then a final ```lean4 block | plan prose, then a final ```lean4 block |
| sampling (card / harness) | temperature 1.0, top_p 0.95 (Goedel protocol; what `lean_gen` hard-codes by default) | card gives none; use the same 1.0 / 0.95 for comparability |
| context | 40,960 (Qwen3) | config 65,536 (YaRN x16, orig 4,096), card says 32K: run with `--max-model-len 32768`, cap <= 30,000 |
| repair prompt | the Goedel round-k correction prompt works as for the 8B (model is the same family and trained for it; 90.4% "self-correction mode") | none published; round 0 only |

The Goedel format of `extras/vllm_rollout/lean_prompts.py` serves Goedel-32B exactly (same family, same template) and
DeepSeek-7B up to the one-newline fence difference above. What is needed is in section 5.

## 5. Design note: changes for `extras/vllm_rollout/` (another lane's files; NOT edited here)

1. **Double BOS for DeepSeek (correctness).** `lean_gen.prepare()` does `ids = list(tokenizer.encode(text))` (default
   `add_special_tokens=True`) on text produced by `apply_chat_template(tokenize=False)`. For Qwen3 that is a no-op (no BOS). The
   DeepSeek template already prints `bos_token`, and `encode` would prepend a second BOS id 100000. Change: a
   `bos_in_text = tokenizer.bos_token is not None and text.startswith(tokenizer.bos_token)` test and
   `tokenizer.encode(text, add_special_tokens=not bos_in_text)`; apply the same expression in `run_fidelity`'s id check and in
   `prompt_render_sha` (so the sha pins the ids actually sent). Note `lean_gen` sends `prompt_token_ids`, not text, so vLLM adds
   nothing itself. Without this fix DeepSeek-7B generates with a doubled BOS: a silent quality loss, not an error.
2. **Teacher provenance in every record** (needed for the license ledger, section 7). `build_record(..., extra=...)` already takes
   `extra`: add `--teacher-id` (hub repo), `--teacher-license` (hub string) and `--teacher-card-rev`; write
   `{"teacher": {"repo", "revision", "license", "role": "teacher"}}` into each record and into `write_manifest`. `model_rev_of`
   already supplies the snapshot sha. Make `resume_conflicts` refuse to resume a file under a different teacher id.
3. **Engine flags for the 32B**, as CLI options passed through to `LLM(...)` (today `LLM(...)` is called with a fixed kwarg
   set): `--kv-cache-dtype {auto,fp8}` (default auto), `--enable-chunked-prefill` (leave vLLM default), and a default
   `--max-num-seqs 16` for the 32B (128 is the 8B default; with room for ~12 sequences a larger value only grows the
   preemption/recompute churn). `--gpu-mem-util 0.94` is worth one smoke try, with the NVML guard the lane already has.
4. **`--max-model-len`**: default 40,960 is right for Goedel-32B (Qwen3 limit) and **wrong** for DeepSeek-7B (use 32,768). The
   existing check "max_model_len above the model's position limit raises" must read `max_position_embeddings=65536` yet the
   card limit is 32K: add an explicit `--max-model-len 32768` in the launch command rather than trusting the config.
5. **No change** to extraction (`extrac_code`, last ```lean4 fence), `lean_code_for_record`, `problem_check` or the sampling
   defaults: both teachers answer in the Goedel output shape. The `kimina` format and `kimina_final_answer` are irrelevant here.
6. **Cap**: use `--cap-tokens 16384` for the first pass. Goedel reports their protocol at 32k; at cap 16k the 8B hit the cap in
   8.2% of miniF2F samples and the hard band will be higher (assume ~35%). Rejected-by-cap samples are not proofs and cost the
   most, so a second pass at 32k only on never-solved statements (section 6).

7. **Sampler parity**: pass `generation_config="vllm"` to `LLM(...)` (or explicit `top_k`) so a model's own `generation_config.json` (3.2) cannot change the sampler.

## 6. Plan: what each teacher attempts

Definitions (from the Phase-0a supply audit, `scripts/p2/supply/`): the band is every pool statement that passed the elaboration
check and the misformalisation screen, with a profile of OUR 8B at n = 16-32.
* **Marginal band M**: 8B pass rate in (0, 0.25]. Real proofs exist, the 8B finds them rarely; a stronger teacher's proofs add
  style and a higher hit-rate signal. Highest expected yield per token.
* **Never-solved band N**: 0 / 32 for the 8B, and not flagged misformalised (Goedel: >80% of unsolved Pset statements were
  misformalised; a teacher "proof" of a vacuous or wrong-statement theorem is worthless, so the screen comes first).

| stage | teacher | statements | n | cap | rate (est.) | mean tokens | box-h | expected yield |
|---|---|---|---|---|---|---|---|---|
| T0 smoke / calibration | Goedel-32B | 64 from M, round 0 | 2 | 16,384 | measure | measure | **~1.5** (incl. load ~4 min) | replaces every rate in this note |
| T1 marginal | Goedel-32B | M (B_M, expect a few hundred) | 4 | 16,384 | ~145 tok/s | ~8,000 | `B_M x 4 x 8,000 / 145 / 3600`: **B_M=300: 18 h; 500: 31 h** | high: expect pass@4 of 30-60% on M |
| T2 never-solved | Goedel-32B | N screened (B_N) | 8 | 16,384 | ~145 tok/s | ~11,000 | **B_N=300: 51 h; 500: 84 h** | low: single-digit % of N; each proof is a new problem |
| T3 correction round | Goedel-32B, Goedel correction prompt | N statements with failures that have compile errors (feedback present) | 1 per failed parent | 16,384 | ~145 | ~9,000 | ~25% of T2 | adds the "self-correction" lift (88.0 to 90.4 on miniF2F, a reported figure) |
| T4 (optional, license-gated) | DeepSeek-Prover-V2-7B | M + N | 4 | 16,384 | ~365 tok/s | ~7,000 | B=800: 15 h | different proof style; only if 1.1 is resolved |

Budget rule of thumb: the 32B costs ~7 box-h per 1M generated tokens (145 tok/s), so the SFT-worth of T2 must be weighed against
the SOTA_PLAN line items (Phase 1 ~200 box-h). **Recommended**: T0 then T1 (≈20-30 box-h), then T2 only on the screened subset
of N with a prior (e.g. classifier score) and B_N <= 200 (~35 h), stop early with the lane's early-stop when yield per box-h
drops below the 8B's own self-distillation yield. All stages run strictly serially with the 8B generation (hostguard lock:
never two heavy jobs), and stage-checkpoint at every `lean_gen` flush (the writer already flushes every 8 records).

Throughput honesty: 130-160 tok/s is the model's estimate with eff calibrated on the 8B. Two unmeasured risks: (a) NCCL all-reduce
at 128 per step with only ~10 sequences is latency-bound and may be worse than eff 0.46 suggests (could be 100 tok/s); (b) fp8-KV on
Ampere may be slower or unsupported. T0 resolves both. If T0 reads below ~100 tok/s, T1 halves (B_M x n = 600 samples) and T2 is dropped.

## 7. How teacher proofs enter training

1. **Verified only by OUR frozen verifier** (`docs/LEAN_VERIFIER.md`, hash-pinned): the teacher's own claim of success, its own
   compile feedback, and any third-party verifier are ignored. The accepted set is exactly what `verify_generations.py` accepts
   at the frozen verifier hash (300 s, axiom walk, statement-fidelity check, `problem_check` re-insertion of the ORIGINAL statement).
2. **Decontaminated before training** with the same pipeline as every other source (`align.data.decontam`, elaborated-statement
   hashing + MinHash + the base-model membership check): the PROBLEM must be absent from miniF2F valid/test, ProofNet, PutnamBench
   and every eval set; teacher output does not launder a contaminated statement. Teachers were trained on data we do not control
   (Goedel-V2 on its own Workbook/Pset; verify the Goedel-Pset overlap with the pool statement sha, not just by name). Proof text
   is also MinHash-checked against the eval proof sets (miniF2F solution zips) so a memorised published proof cannot enter.
3. **Provenance on every row**: `{source: "teacher", teacher_repo, teacher_revision, teacher_license, card_revision,
   prompt_format, temperature, top_p, cap, seed, verifier_hash, problem_ancestry}`. `build_sft_data.py` gets a `--source-tag`
   so teacher rows are a separate, countable stream; per-problem cap (`--max-per-problem 4`) applies across self + teacher rows.
4. **Separate arm in the contrasts**: teacher rows are added as their own SFT arm (self-only vs self+teacher, same token budget)
   so a gain is attributable and a loss is not hidden by the pooled mix. Same eval, same verifier, same seeds, matched row
   counts; the teacher stream is registered in the pre-registration BEFORE generation (docs/PREREG_SOTA.md) with its
   pass/fail gate (it must not lower self-distillation accepts/box-h).
5. **Licenses recorded and checked at release**: `docs/TEACHERS.md` (this file) plus a machine-readable ledger
   `teachers_ledger.json` written by the lane from the record `teacher` blocks; the release script refuses a model whose training
   mix has a teacher with a non-permissive or unresolved license (DeepSeek until 1.1 is decided). Goedel-V2-32B is Apache-2.0
   with no output clause: attribution only (NOTICE entry). Distillation from a model whose own base is Qwen3-32B (Apache-2.0)
   adds no further restriction.
6. **Selection**: drop teacher proofs whose length exceeds the SFT sequence budget (16,384), those that hit statement-rewrite
   paths, and those that use `sorry`/axiom tricks (verifier already rejects). Keep at most 2 distinct proofs per problem from the
   teacher (diversity over volume), shortest-accepted-completion first as the 8B pipeline does.