align: a torch-only post-training stack with a Lean 4 verifier in the loop

align is a post-training library (SFT, DPO, PPO, GRPO / Dr.GRPO / DAPO-clip, CISPO, expert iteration) whose runtime dependencies are only torch, triton, numpy and safetensors. It contains a strict Lean 4 proof verifier, FSDP2 training with coordinated stop/resume, a dropless MoE (OLMoE) and a Qwen3 model path. This repository is a code snapshot, not a model checkpoint. The measured results below come from running this code on one 4-GPU box.

Headline (measured, 2026-10-24 to 2026-10-26): three rounds of verifier-filtered expert iteration on Goedel-Prover-V2-8B produced no measurable gain on miniF2F-valid. Solved@8 went 188 (base) → 188 → 187 → 185 of 226. Base vs round 3 has an exact McNemar p of 0.51. Treat this card as a record of the engineering and of a negative result, not as a SOTA claim.

1. TL;DR product sheet

What it is	Post-training library + Lean 4 verifier + evaluation harness (code snapshot; git bundle with full history)
Code in this repo	code/ = working tree at commit f8dfa503 (2026-10-19, see COMMIT); align.bundle = full git history
Runtime deps	torch, triton, numpy, safetensors only. An AST firewall test enforces this (tests/test_dependency_firewall.py). vLLM and W&B run in separate venvs under extras/ and only exchange files with the trainer.
Algorithms implemented	SFT (masked CE, global token-mean); DPO (sigmoid, ipo, sigmoid_norm, dpop) with precomputed reference log-probs; PPO with LoRA, a value head, GAE and PRM step rewards (clip_delta); GRPO (vendored from open-instruct, Dr.GRPO constant denominator, DAPO clip-higher, ρ correction); CISPO + FP32 LM head; single-turn Lean RL (cispo / dr_grpo / ei); expert iteration with weight averaging
Models exercised	Goedel-Prover-V2-8B (Qwen3, 8.19B; LoRA r64), OLMoE-1B-7B-0125 (6.92B MoE; full FT), tiny Mistral/OLMoE test models
Verifier	Lean 4.9.0-rc1 + Mathlib d1d1e4b7 + REPL v4.9.0-rc1. Accepts 177/178 known-good proofs and 0/61 adversarial ones; a naive compile-only check accepts 51/61.
Best measured eval (base model through this harness)	Goedel-Prover-V2-8B on miniF2F-test: pass@8 78.7% (192/244) at a 16k cap; pass@32 82.8% (202/244) at a 40k cap. The published figure is 84.6% pass@32.
Trained-model result	Expert iteration, 3 rounds (LoRA SFT on 374-442 self-generated verified proofs per round): no gain on miniF2F-valid (section 6)
Compute	One host with 4 GPUs of 23 GB each, connected over PCIe with no NVLink. Campaign1 stage markers record 27.2 box-hours across 3 rounds (round-1 generation not included).
Licence	Apache-2.0 (code). Third-party data licences are in section 10.

2. Library details and mechanism

• Model code: dense Mistral and Qwen3 (with QK-norm and GQA), plus OLMoE (dropless top-k MoE). The MoE combine is fixed-order: see the bug in section 7. Parity with transformers: OLMoE fp32 max |Δlogit| is 1.4e-5 to 3.0e-5, with top-1 agreement 74/74 and router top-8 sets 100% on all 16 layers.
• Trainer: FSDP2 with bf16 params and fp32 reduce-scatter. The optimizer is an in-repo block-wise 8-bit AdamW (adamw8bit) with per-rank optimizer files. A SIGTERM or wall-clock stop halts every rank at the same optimizer-step boundary. Checkpoints are fsynced and checked for completeness. Distinct exit codes 80-83 survive torchrun through HALT.json, and scripts/supervise.py relaunches the run after a crash.
• Rollout: vLLM in extras/vllm_rollout with its own venv; the trainer exchanges JSONL with it. There is also a native paged-KV engine (CPU-validated only).
• Verifier (align/verify/lean/): a strict layer (lexical gate, exact statement match, axiom whitelist {propext, Classical.choice, Quot.sound}, header checks), a REPL pool with memory and time caps, and a 180 s budget per proof. Timeouts, crashes and memory kills count as "no signal" and are never scored as failures.

flowchart LR
  subgraph Data
    P[Problem JSONL<br/>HF-streamed pool<br/>decontaminated] --> S[select_by_band<br/>pass-rate band 0..0.75]
  end
  subgraph Rollout["extras/vllm_rollout (own venv)"]
    G[lean_gen.py<br/>vLLM TP=4, T=1.0, top_p 0.95]
  end
  subgraph Verify["align/verify/lean"]
    V[strict verifier<br/>Lean 4.9.0-rc1, 180 s<br/>axiom whitelist, statement match]
  end
  subgraph Train["align/train + align/rl (torch only)"]
    SFT[SFT: LoRA r64, adamw8bit, FSDP2]
    RL[GRPO / CISPO / PPO<br/>Dr.GRPO denominator, rho-correction]
    DPO[DPO: fused chunked kernel,<br/>precomputed ref log-probs]
  end
  AVG[weight average<br/>0.7 ft + 0.3 base]
  E[eval_report.py<br/>pass@k, cluster bootstrap,<br/>exact McNemar]
  S --> G --> V
  V -- accepted proofs --> SFT --> AVG --> G
  V -- rewards --> RL
  AVG --> E

flowchart TB
  T[torchrun x4] --> R0[rank 0..3: Trainer]
  R0 -->|every boundary: MAX-reduce stop / non-finite flags| B{stop?}
  B -- no --> O[adamw8bit step, grad clip 1.0, tripwires]
  B -- yes --> C[checkpoint: model.safetensors + optimizer_rank r.pt + RNG, fsync, completeness check]
  C --> H[HALT.json exit 80-83 or 143]
  H --> SUP[supervise.py: relaunch only after a non-HALT crash that made progress]
  SUP --> T

3. Training data

This is a library card, so the data listed here is the data of the measured runs.

Use	Source (HF id)	Licence	Rows used	Notes
EI campaign pool	viai957/lean-prover-data:problems/train_pool.jsonl	mixed, per row	1,992 kept of 2,000 read	8 dropped for informal overlap with a protected benchmark
EI campaign pool	viai957/lean-prover-data:supply/screen_v1.jsonl	mixed, per row	3,948 kept of 4,000 read	49 informal overlaps and 3 duplicates dropped
Pool by origin	goedel-pset-v1 1,992; rl-goedel-pset-l45 997; numinamath-lean-sol 989; nemotron-math-proofs-v1 989; formalmath-all 973	MIT / MIT / Apache-2.0 / CC-BY-SA-4.0 / MIT	5,940 total	runs/campaign1/pool.jsonl
Protected (never selected)	miniF2F-test, MOBench	MIT / own	-	protected_problems in the round manifests; the EI driver refuses test-split selection
Model selection	miniF2F-valid	MIT	226	all stop decisions use this split
OLMoE smoke	PRM800K SFT shards from nano-mistral-o1, re-tokenized	MIT	320 rows, 640-968 tokens	control-plane test only

SFT data per EI round: up to 4 of the shortest verified proofs per problem, from n=8 samples at a 16k cap. The selection order is in-band (0 < p ≤ 0.75), then unmeasured, then never-solved (at most 60), truncated at 300 problems.

Round	in-band selected	unmeasured selected	never-solved selected	SFT rows	problems with rows	completion tokens	prompt tokens
1	115	185	0	442	135	1,642,463	111,922
2	107	193	0	374	120	1,377,760	97,007
3	96	204	0	398	127	1,523,369	96,571

No never-solved statement was ever selected, because in-band plus unmeasured problems always filled the 300 slots.

4. Training procedure

Objectives as implemented

SFT (align/train/sft_loss.py, loss_normalization = "global_token_mean"). The loss mask $m_t$ zeroes prompt and pad tokens. The denominator is all-reduced over the accumulation window and over ranks:

DPO (align/kernels/fused_dpo.py). With $\Delta=(\log\pi_\theta(y_w)-\log\pi_\theta(y_l))-(\log\pi_{\text{ref}}(y_w)-\log\pi_{\text{ref}}(y_l))$ and reference log-probs precomputed as constants:

$${\mathcal{L}}_{\text{DPO}}=-\log \sigma (\beta \mathrm{\Delta }),{\mathcal{L}}_{\text{DPOP}}=-\log \sigma (\beta (\mathrm{\Delta }-\lambda \max (0,\log {\pi }_{\text{ref}}(y_w)-\log {\pi }_{\theta }(y_w))))\backslash mathcal\{L\}\_\{\backslash text\{DPO\}\}=-\backslash log\backslash sigma(\backslash beta\backslash Delta),\backslash qquad\; \backslash mathcal\{L\}\_\{\backslash text\{DPOP\}\}=-\backslash log\backslash sigma\backslash big(\backslash beta(\backslash Delta-\backslash lambda\backslash max(0,\backslash log\backslash pi\_\{\backslash text\{ref\}\}(y\_w)-\backslash log\backslash pi\_\backslash theta(y\_w)))\backslash big)$$

The defaults are $\beta=0.1$, $\lambda=50$ (dpop is a tripwire response, not the primary variant), and an optional chosen-side NLL term.

GRPO / Dr.GRPO (align/rl/grpo_loss.py, vendored from allenai/open-instruct @ 8759c91). Advantages are centred within each group and not divided by the standard deviation: $A_i=r_i-\frac1G\sum_j r_j$. With $\rho_t=\pi_\theta/\pi_{\text{old}}$:

$$\mathcal{L}=-\frac{1}{C}\sum _{i,t}\min \text{\hspace{0.17em}⁣}({\rho }_t{A}_i,\text{ clip}({\rho }_t,1-{ϵ}_l,1+{ϵ}_h)A_i)+\beta \widehat{\text{KL}}\backslash mathcal\{L\}=-\backslash frac\{1\}\{C\}\backslash sum\_\{i,t\}\backslash min\backslash !\backslash big(\backslash rho\_t\; A\_i,\backslash \; \backslash text\{clip\}(\backslash rho\_t,1-\backslash epsilon\_\{l\},1+\backslash epsilon\_\{h\})A\_i\backslash big)+\backslash beta\backslash ,\backslash widehat\{\backslash text\{KL\}\}$$

$C$ is a constant global denominator (prompts × G × max_len). The defaults are $\epsilon_l=0.2$ and $\epsilon_h=0.272$ (DAPO clip-higher). The A3 gate requires $\beta=0$ and refuses to launch otherwise, except $\beta=10^{-4}$ under the explicit allow_kl_ablation flag (the pre-registered collapse-response ablation). A stop-gradient engine-mismatch factor $\pi^{\text{train}}{\text{old}}/\pi^{\text{infer}}{\text{old}}$ is applied and masked.

CISPO (align/rl/cispo.py, MiniMax-M1 Eq. 4-5). The clipped importance weight is a stop-gradient constant, so no token's gradient is zeroed. There is no KL term. An optional FP32 LM head (chunked and checkpointed) reduces the mismatch between sampler and trainer:

PPO with process rewards (align/ppo/, ported from mistral-prm-ppo). The objective is a clipped surrogate (cliprange 0.2) plus a clipped value loss (0.2) plus a k3 KL. GAE uses separate $\lambda_{\text{actor}}$ and $\lambda_{\text{critic}}$, and $\gamma=1$ is enforced. PRM step scores $p_j$ are shaped with clip_delta: $c_j=\min(p_j-\eta,0)$, $d_j=c_j-c_{j+1}$ (potential-based), with $\eta$ an absolute probability (0.80 in the draft config).

Expert iteration (campaign1, scripts/p2/expert_iteration.py). Each round $k$ runs four steps:

1. Select problems by pass-rate band.
2. Sample n=8 proofs at a 16k cap and verify them.
3. Run LoRA SFT on the verified proofs.
4. Average the weights against the original base: $W_{k}=0.7,W^{\text{ft}}{k}+0.3,W{0}$.

The run stops on a regression, when solved@8 is at or below the best so far minus 3 (max_regress). It also stops on a plateau, when each of the last 2 rounds fails to beat the earlier best by at least 2 problems (min_gain, patience). Campaign1 stopped after round 3 on regression (185 ≤ 188 − 3) and kept round 1.

Hyperparameters (campaign1 SFT, configs/p2_sft.toml + round manifests)

Parameter	Value
Base	Goedel-LM/Goedel-Prover-V2-8B @ dfd02e62 (Qwen3, 8,190,735,360 params, 36 layers)
Adapter	LoRA r=64, α=128, dropout 0. Targets: q,k,v,o,gate,up,down. 175M trainable params (2.1%)
Optimizer	adamw8bit, lr 2e-5, betas (0.9, 0.95), wd 0, clip 1.0
Schedule	10% warmup, cosine to 0, 2 epochs; 28 / 24 / 27 optimizer steps (rounds 1/2/3)
Batch	micro-batch 1 × seq_len 18,432 tokens (packed token budget), grad_accum 2, 4 ranks → 8 micro-batches per step
Precision / parallelism	bf16, FSDP2, sdpa attention, per-rank optimizer state
Weight averaging	ft_weight 0.7, anchored to the original base
Eval	miniF2F-valid, n=8, cap 30,000, T=1.0, top_p 0.95, seed 0, verifier budget 180 s

Compute (stage markers in runs/campaign1/ei/round_0*/round_manifest.json)

Round	train (s)	gen+verify (s)	eval (s)	export+average (s)	total (h)
1	2,223	55*	13,110	450	4.40
2	1,977	21,868	14,645	369	10.80
3	2,168	24,778	15,825	416	12.00

*Round-1 generation ran during earlier failed attempts and is not in the marker. Recorded total: 27.2 h.

Hardware: 4 GPUs of 23 GB each over PCIe, with no NVLink. NCCL uses the SHM transport at about 4 GB/s. docs/MEASUREMENTS.md records the GPUs as A10G (sm_86) on 2026-10-12. A project note dated 2026-10-25 records an nvidia-smi reading of L4 (sm_89). The campaign manifests do not record the GPU model.

5. Training curves

Figure 1. LoRA SFT for EI rounds 1-3. Left: token-mean CE, averaged over the 4 ranks per micro-step. Middle: learning rate actually applied. Right: pre-clip gradient norm at optimizer steps. Source: the local W&B history runs/campaign1/wandb/wandb/run-20261023_212613-0ca1a6eafc40/run-0ca1a6eafc40.wandb (keys sft/*, 632 rows = 158 micro-steps × 4 ranks). The checkpoint directories were pruned after export, so W&B is the only surviving log.

The loss is low from the first step, because the data is the model's own verified output: the rank-mean is 0.18 / 0.15 / 0.11 at the first micro-step of rounds 1/2/3. The loss is noisy within an epoch and does not trend down. The gradient norm stays between 0.017 and 0.034, so the clip at 1.0 never binds.

Figure 2. OLMoE-1B-7B-0125 full-FT smoke run on 4 GPUs (FSDP2, adamw8bit, load balancing off, lr 1e-5, 16,384 padded tokens per step): mean loss per optimizer step and pre-clip gradient norm. Values are transcribed from docs/MEASUREMENTS.md section (g). The raw history.jsonl files were deleted with the checkpoints. This run tests the control plane and makes no claim about convergence.

No RL (GRPO / CISPO / PPO) or DPO run has been executed with this code on GPUs, so there are no reward, KL or clip-fraction curves.

6. Evaluation

6.1 Harness validation: base model on miniF2F-test (244)

Figure 3. Goedel-Prover-V2-8B through the align harness. Sources: docs/evidence/p2_baseline_2026-10-13/report.md and docs/evidence/sota_repro_2026-10-14/report.md. The dashed line is the published 84.6% pass@32 (docs/SOTA_TARGETS.md).

Run	n/problem	cap	pass@1 [95% cluster bootstrap]	pass@2	pass@4	pass@8	pass@32	length-capped	mean tokens
base16k	8	16,384	62.1% [57.0, 67.3]	70.1%	75.4%	78.7% (192/244)	n/a	5.8%	4,921
base40k_n32	32	40,960	62.8% [57.9, 67.7]	n/a	n/a	79.7%	82.8% (202/244)	2.3%	5,669

Our pass@32 is 202/244 and the published figure is 84.6% (≈207/244). The gap is 5 problems. 391 of 7,808 samples hit the 180 s verifier timeout, while the published compile budget is 300 s. A re-check of timed-out samples at 300 s accepted 0 of the first 82, so the baseline stays at 202.

6.2 Hill-climbing: expert iteration on miniF2F-valid (226)

Figure 4. Solved@8 (Wilson 95%) and pass@1 (cluster bootstrap over problems, 2,000 resamples, seed 0), all at n=8, cap 30,000. Sources: runs/campaign1/ei/round_0{1,2,3}/eval/ver_n8_c30000.jsonl and the base run ProofForge/runs/p5_eval/base/ver_n8_c30000.jsonl (run 2026-10-26 with the same lean_gen.py, sampling args and prompt render hash 83d0bbb9…). The only verifier-config difference is the worker count (2 vs 8).

Model	solved@8 [Wilson 95%]	pass@1 [bootstrap 95%]	pass@2	pass@4
Base Goedel-Prover-V2-8B	188/226 = 83.2% [77.8, 87.5]	71.8% [66.6, 77.0]	77.6%	80.7%
EI round 1	188/226 = 83.2% [77.8, 87.5]	71.9% [67.0, 76.7]	78.2%	81.6%
EI round 2	187/226 = 82.7% [77.3, 87.1]	71.1% [65.9, 76.2]	77.2%	80.5%
EI round 3	185/226 = 81.9% [76.3, 86.3]	72.0% [66.9, 76.8]	77.9%	80.5%

Paired solved@8 comparisons (exact two-sided McNemar on the 226 problems):

Comparison	only A	only B	p
base vs r1	2	2	1.00
r1 vs r2	3	2	1.00
r2 vs r3	5	3	0.73
base vs r3	6	3	0.51

Figure 5. Unbiased pass@k (n=8) on miniF2F-valid for the base and each EI round, from the same verification files as Figure 4.

6.3 Verifier quality

Figure 6. Pre-registered ceiling test, 2026-10-12 (docs/evidence/lean_ceiling_2026-10-12/registered.log, result.json, table sha256 61636c71…).

Check	Result
Known-good accepted (Lean-workbook-proofs slice)	177/178 = 99.44%, Wilson 95% [96.89, 99.90]. The one miss is a 180 s timeout.
Adversarial accepted	0/61. A naive compile-only check accepts 51/61.
Frozen verifier f1dd9e78 (2026-10-19)	178/179 known-good (docs/SOTA_PLAN.md 4.3; the artefact is untracked)
Throughput, 8 warm workers	0.57 proofs/s on unique statements (p50 1.97 s, p90 21.4 s); 4.38 proofs/s in the GRPO shape (12 statements × 8 samples)
vs Kimina Lean server, 741 items (docs/results/kimina_agreement_report.json)	485/485 strict accepts pass Kimina as well. Kimina compile-only passes 40 adversarial items that strict rejects. 0 Kimina false rejects. Kimina is not adopted: the gated pipeline is about 52% slower.

6.4 Systems measurements (docs/MEASUREMENTS.md)

Figure 7. One MoE layer at OLMoE shape (E=64, top-8, d=2048, bf16), forward+backward median of 10 runs, from docs/MEASUREMENTS.md section (c). torch._grouped_mm takes the fallback path on sm_86 and is only 1.06-1.13× faster than the loop.

Measurement	Value
2-rank FSDP2 + adamw8bit, SIGTERM to one rank, then resume	Final params bit-identical (0 of 2,885,888 elements differ). A negative control with swapped optimizer shards is detected.
NaN on one rank	Both ranks halt with exit 81 within about 1.3 s, with no NCCL hang
OLMoE-1B-7B, 4-GPU FSDP2 SFT	14.79 s per micro-step; 277 padded tok/s; 0.53 TFLOP/s per GPU. 92% of the step is NCCL over SHM.
OLMoE SIGTERM, supervisor relaunch, resume	Max
Qwen3-8B LoRA SFT throughput (configs/p2_sft.toml)	2,152 padded tok/s at 16,384-token micro-batches; 15.84 GiB allocated peak
vLLM generation, TP=4 (docs/evidence/p2_baseline_2026-10-13/gen_minif2f_c16384.jsonl.manifest.json)	876 tok/s end to end on the 16k miniF2F-test baseline: 9,605,934 tokens, 1,952 samples in 10,966 s (3.05 h)

7. Results discussion and lessons

• Expert iteration on a strong prover was flat. Round 1 matched the base exactly at solved@8 (188 vs 188, 2 discordant each way), and later rounds drifted down without significance. Three explanations are consistent with the data, and none is tested in isolation: (a) the SFT data was the model's own short verified proofs, mostly on problems it already solved; (b) never-solved problems were never selected (0 in every round); (c) the 0.7/0.3 weight averaging toward the base damps any change. The flat result led the plan to drop more rounds and move to repair/feedback arms.
• A real nondeterminism bug that only real weights could show. bf16 index_add_ atomics in the MoE combine picked different expert sets on identical inputs: 5 of 5 repeats were distinct, and the step-1 grad norm was under-reported by up to 2.7×. A fixed-order combine with fp32 accumulation fixed it, and repeats became bit-identical.
• Silent rank duplication. Dense sft.py / pretrain.py gave every rank the same batches, so 4 GPUs trained like 1. This is fixed with a DistributedBatchSampler. Before the fix, multi-GPU dense SFT results from this tree are invalid.
• Scheduler bug in the predecessor. The predecessor trainer (nano-mistral-o1) logged a decaying LR but never applied it. All of its runs used a constant LR. align applies the scheduled LR and has a test that pins it, so align runs are not LR-comparable to nano-mistral-o1 runs.
• This PCIe box is comm-bound. FSDP costs 24× / 10× / 5.6× the compute time at 1k / 4k / 8k-token micro-batches. The cheapest fix is a larger micro-batch, not custom GEMM kernels.
• Evaluation protocol matters at the 1-3 problem scale. Protocol choices are about the same size as the effects measured: on miniF2F-test, the cap alone (16k vs 40k) moves pass@8 from 78.7% to 79.7%, about 2 problems, while the EI effects were 0-3 problems. A 300 s re-check of 82 samples that timed out at 180 s recovered none.

8. Intended use, limitations, risks

• Intended use: research on verifier-in-the-loop post-training for Lean 4 provers on small clusters, and as a reference implementation of the listed objectives with tests (168 entries in code/tests/ at the shipped snapshot; 1,608 CPU tests passed at 654c20c, per the repo README).
• Not measured: GRPO, CISPO, PPO and DPO on GPUs with this tree; multi-turn Lean RL; the native paged-KV and TP engines on GPU; kill -9 during a save; expert parallelism end to end; full-parameter fine-tuning of a 7-8B dense model (campaign1 used LoRA); LBL-on versus LBL-off.
• Limitations: the PPO config has unresolved [TBD] fields, and the PRM checkpoint it needs does not exist. GRPO resume is not wired into scripts/grpo.py. Distinct ranks still write to the same history.jsonl (rank-local logging). There is no OS sandbox on the default verifier path: a sandbox exists, but it is not wired in.
• Risks: a Lean verifier can be fooled. The adversarial set is 61 items, and an upstream kernel issue (lean4#14576) has not been tested against this pin. Do not treat "accepted" as a proof of correctness without independent re-checking.
• Host safety: the jobs assume scripts/hostguard.py cgroup caps. Running them without the caps on a shared box can OOM it.

9. Reproducibility

git clone align.bundle align && cd align        # or use code/ (commit f8dfa503); see the campaign note below
uv venv .venv && uv pip install -e ".[dev]"     # torch, triton, numpy, safetensors, pytest
.venv/bin/python -m pytest tests/ -q -m "not gpu and not oracle and not slow"

# Lean toolchain (Lean 4.9.0-rc1, Mathlib d1d1e4b7, REPL v4.9.0-rc1)
bash scripts/lean_setup.sh
.venv/bin/python scripts/lean_ceiling_test.py           # verifier ceiling (pre-registered table)

# Baseline eval (vLLM in its own venv)
.venv/bin/python scripts/p2/launch_baseline.py ...      # see docs/P2.md
.venv/bin/python scripts/p2/eval_report.py ...          # pass@k, bootstrap, McNemar

# Expert iteration campaign (4 GPUs). REQUIRES commit >= de55434 -- NOT in this snapshot.
# scripts/p2/campaign.sh was added after f8dfa503 (in 2eb6baa), so this line will not run from code/.
bash scripts/p2/campaign.sh                             # wraps scripts/p2/expert_iteration.py, configs/p2_sft.toml

Item	Value
Code snapshot in this repo	f8dfa503f15d4498f43a6e7e579d450f0869bc95 (2026-10-19)
Code that produced campaign1	local tree at or after de55434 (2026-10-24; the fix that let round-1 train). Not in this snapshot: re-upload needed. Local HEAD at card time: 4a6a9f6.
Pre-registration	docs/PREREG_SOTA.md, docs/evidence/prereg/prereg_sota_v1.json (file sha256 172b0c48…); bundle digest 58bb39ed… recorded in prereg_sota_v1.sha256.txt (OpenTimestamped, .ots)
Model revisions	Goedel-Prover-V2-8B dfd02e62; OLMoE-1B-7B-0125 9b0c1aa8
Raw hashes	docs/evidence/*/raw_sha256.txt

Note: the HF snapshot predates the campaign1 code and results. Run outputs (runs/) are not in this repository.

10. Related repositories, licence, citation

• Expert-iteration checkpoints: Goedel-Prover-V2-8B-EI-campaign1-r1, -r2, -r3
• Data: viai957/lean-prover-data
• Predecessors (the code that align consolidates): nano-mistral-o1-sft, nano-mistral-o1-dpo-arm-a, nano-mistral-o1-dpo-arm-b, nano-mistral-o1-grpo-stageb-step48, mistral-7b-v0.3-prm800k-prm-ppo-math
• Downstream: Goedel-Prover-V2-8B-VLG-planner-sft-lora

Licence. Code is Apache-2.0 (code/LICENSE); attributions are in code/NOTICE. The GRPO loss is vendored from allenai/open-instruct (Apache-2.0). Statement sources: Goedel-Pset-v1 and RL-Goedel-Pset-Level-4-5 are MIT; FormalMATH-All is MIT; NuminaMath-LEAN-Sol is Apache-2.0; Nemotron-Math-Proofs-v1 is CC-BY-SA-4.0 (share-alike). Goedel-Prover-V2-8B is Apache-2.0. miniF2F is MIT and is used for evaluation only.

@misc{align2026,
  title        = {align: a torch-only post-training stack with a Lean 4 verifier in the loop},
  author       = {viai957},
  year         = {2026},
  howpublished = {\url{https://huggingface.co/viai957/align}},
  note         = {Code snapshot f8dfa503; expert-iteration campaign1 results (negative)}
}