SOTA plan v3.1: an open 8B Lean 4 prover, published like Leanstral 1.5 (2026-10-14)

Revision history (v3.1, same day: Codex plan findings re-verified against v3, .tmp/audit_2026-10-14/codex/P13-plan.verdicts.json; amendments marked [v3.1]):

v1 proposed a sequential staircase of levers.
v2 applied an independent Codex review (docs/evidence/codex_review_2026-10-14.md): controlled contrasts, one endpoint, evaluation reserved first.
v3 applies a line-by-line verification of the code (12 units) and a first-principles plan review, both adversarially re-verified (docs/evidence/deep_verification_2026-10-14.md). What changed in v3:
- Estimand. The primary is now the unbiased pass@32 from n = 64 samples with a paired sign-flip test. Binary McNemar is kept as a secondary. Re-run simulation: power at +1.4 pp rises from 7% to 30%, and at +3.6 pp from 42% to 96% (.tmp/audit_scratch/power_sim3.py, reproduced).
- Data supply. The ~220-statement band left in the pool after the base model trained on its source cannot carry Phases 1-2. A supply audit, a CPU difficulty/fidelity classifier (our DeepSeekMath fastText analogue) and a dev set of at least 1,000 problems come first.
- Mechanism contrasts. These run on a base with headroom (Kimina-Prover-Distill-8B, SFT-only). The winning recipe is then applied once to Goedel-8B as the SOTA attempt.
- Inference-time levers first. Correction, subgoal repair and the agentic loop are promoted, and class B becomes co-primary.
- New controls. An A/A null run, a per-arm alpha sweep and a temperature-matched ALF control.
- Bug paper. It gets a confirmatory ground-truth benchmark (RustSec / fix commits / mutants), bounded-checker baselines (Kani, proptest, cargo-fuzz) and blinded adjudication.
- Publication blockers (Phase 0): LICENSE, externally time-stamped pre-registration, a fresh post-cutoff benchmark, and at least 3 training seeds for headline contrasts.
- Success estimate revised to about 10-15% for a significant class-A gain, unless the supply audit raises the prior.

Scope (decided): post-training only, starting from Goedel-Prover-V2-8B, on this box (4x A10G, shared, no rented compute). External numbers are self-reported (SR) unless marked IR. "Judgment" marks my own estimate.

0. What "publishable like Leanstral" means for us

Leanstral 1.5 makes four kinds of claim: benchmark headlines at stated budgets, cost per problem, a training recipe, and a real-world result (5 new Rust bugs). We match the shape, not the numbers of a 119B MoE with 4M-token agent trajectories. Long agent windows are excluded because of native context, extrapolation quality and throughput. Memory alone is not the reason: ~29 GB of KV at 200k tokens is ~7.4 GB per card under TP=4.

Two papers, decoupled:

Prover paper. Its headline does not depend on winning:
- a protocol-factorial audit of one 8B prover, showing how cap, verifier, statements and sampling move the number (77.9-84.6 across papers);
- controlled mechanism contrasts (data vs RL; mutation vs temperature-matched unmutated; feedback vs restarts), with stated minimum detectable effects (MDEs) and training-seed variance.
The SOTA attempt on Goedel-8B is one pre-registered row of this paper.
Bug-finding paper. A confirmatory recall/FP comparison on a ground-truth Rust benchmark, against an LLM reviewer, bounded checkers and fuzzing. Leanstral's footnote concedes a plain LLM found its showcase bug. Leanstral's precision was 11/47 per flag and 5/47 per distinct bug.

1. Endpoints (pre-registered; text + hash pushed to an external time-stamped store before any test result is read)

Anchor. Goedel-Prover-V2-8B, 202/244 at pass@32 / 40k / 180 s. In Phase 0a it is re-generated at n = 64 and re-verified under the frozen verifier at 300 s (1,200 s sensitivity reported separately).

Primary (co-primary, Holm over the two): [v3.1] a verifier timeout counts as UNSOLVED in the evaluation denominator (reported separately, with the 1,200 s sensitivity); in training a timeout is masked (no signal, never a negative label).

A. Class A (single pass, cap 40k) on miniF2F-test.
- Estimand: mean over problems of the unbiased pass@32 estimate 1 - C(n-c, 32)/C(n, 32) from n = 64 samples per problem.
- Test: paired sign-flip permutation test over problems (10^5 flips), two-sided alpha = 0.05.
- Interval: crate-free, problem-level bootstrap.
B. Class B (trajectory = attempt + up to 2 Lean-feedback repairs, 40k total, cumulative token ledger). Same estimand and test.

Secondary:

exact McNemar on the first-32-samples binary solved@32;
mean pass@1;
ProofNet-test class A.

Exploratory: class C (agentic), PutnamBench class A pass@8.

Noise, decomposed. Benchmark uncertainty comes from the paired test. Generation variability comes from the second-seed anchor in Phase 0a. Training variability comes from at least 3 training seeds for any K-contrast headline and the A/A run (K0).

Class	Protocol	Bar at <=9B	Target
A	whole proof, n = 64, cap 40k	Goedel-V2-8B 84.6% (SR); Pythagoras-4B 86.1% (SR)	significant paired gain over our Goedel-8B anchor; descriptive >= 207. [v3.1] No claim of beating Pythagoras-4B unless a matched-harness Pythagoras-4B n = 64 run (~25 box-h) is added
B	+ 2 Lean-feedback repairs, 40k total	Goedel-V2-8B 86.7% (SR)	significant paired gain over the class-B anchor
C	multi-round + retrieval, R = 4, pass@8	OProver-8B 91.8 / 31.9 / 9.0 (SR, Lean 4.15)	exploratory; agent-vs-agent only

Every number carries the protocol tuple:

benchmark commit and denominator, including the elaborating subset fixed in Phase 0a;
Lean/Mathlib version;
verifier, axiom policy and rewritten-statement count;
n, k, caps and total tokens;
statement version and answer track;
cost split into box-hours, decode/prefill tokens and verifier CPU-hours.

2. Levers (priors)

#	Lever	Evidence	Caveat
L1	Test-time Lean-feedback correction	Goedel-V2-8B 84.6 -> 86.7 (SR, same model)	measure in our harness at matched tokens vs restarts
L6	Agentic: proof bank + subgoal repair (APOLLO-style) + compiler feedback	OProver-8B feedback ablation 91.8 vs 87.7 (SR); APOLLO sample-efficiency	proof bank decontaminated under the same sweep
L2	Verified mutation self-distillation	Pythagoras ALF +6.97 (4B), +5.73 (32B) at ~2M unverified instances	no post-RL/pre-ALF control; temperature confound (T = 1.2); our scale ~100x smaller
L3	Band rejection-sampling SFT	GAR on this model: static GRPO -0.41 (IR baseline), GAR +2.46 (SR)	strong base; 0 to +2.5 pp
L4	Weight averaging / LoRA scale	Goedel: pass@N rises then falls with alpha	swept per arm (K4)
L5	RL on own samples (correction-mode prompts)	DS-Prover-V1.5 RL-over-SFT +1.8..+2.8 not shrinking; Goedel-V1 converges; Leanabell-V2 verifier-in-trajectory +2.9 / +1.0 over vanilla	different mechanisms; RL path must pass the Phase 0b feasibility gate
L7	PKPO advantage transform (pass@k-targeted RL)	PKPO (arXiv 2505.15201): unbiased pass@k gradient; not Lean	optional K1 arm

3. Contrasts (each with a pre-stated MDE; a contrast whose MDE exceeds its prior effect is dropped, not run)

All contrasts are decided on the dev set (Phase 0a: at least 1,000 problems), at matched generated tokens, with at least 3 training seeds for any headline. The dev set is:

held-out in-band pool statements, labelled with samples disjoint from the selection samples, which avoids regression to the mean;
plus ProofNet-dev;
plus miniF2F-valid (226, a filtered subset; disclosed).

Id	Question	Base	Arms	Matched on
K0	A/A null	Goedel-8B	identical recipe, two seeds	everything (gives the null distribution of paired differences)
K5	Inference-time levers	Goedel-8B	2-repair correction vs restart sampling vs agentic (proof bank + subgoal repair)	total tokens per problem; run FIRST
K1	[v3.1] (a) positive-only vs signed updates on the SAME cached rollouts and checkpoint (isolates signed credit); (b) then EI-SFT vs RL pipelines at equal budget, no CISPO-specific claim (+ optional PKPO arm, k = 2-4 with G >= 8, never k = G)	Kimina-Distill-8B (headroom)	(a) same rollouts; (b) L3 vs L5 (vs L5 + L7)	(a) data identical; (b) generated tokens, prompt set; correction-mode prompts excluded from the RL arm (no published Kimina repair prompt) or included in both arms
K2	Is mutation the active ingredient?	Kimina-Distill-8B	verified mutations vs temperature-matched (T = 1.2) own samples on unmutated statements	rows, tokens, temperature; [v3.1] two pre-registered estimands: equal training tokens (production cost reported) and equal total budget (yield free); preceded by a ~200-parent pilot that logs mutator -> elaboration -> verified yields
K4	Averaging / scale	each K1/K2 arm	alpha in {0.5, 0.7, 1.0} (LoRA scale only, no retraining)	reported as curves; arms compared at their own validated alpha
K6	Source-quality ablation (DeepSeekMath analogue)	Kimina-Distill-8B	classifier-selected vs random statements, 0.1B tokens	tokens

The winning recipe chain from K1/K2/K4 is applied once to Goedel-8B. That is the SOTA attempt, scored by the Phase-4 primary.

4. Phases (~20 box-h/day; one box-hour = the whole 4x A10G box for 1 h = 4 GPU-hours)

Phase 0a: measurement and supply (Oct 15-24).

Verifier freeze. Merge the red-team fixes and the deferred verifier findings from the code verification (lexer desync, axiom-walk fail-open, sandbox wiring, orphaned REPLs). Freeze and hash it. Ceiling-test it: known-good accepted, adversarial suite rejected.
Anchor at n = 64, second seed. Re-verify the 202 under the frozen verifier at 300 s and 1,200 s. Report the rewritten-statement count.
Environment coverage. Elaborating subsets of ProofNet-test and PutnamBench, fixed and disclosed. The ProofNet-dev split is built.
Supply audit (~3 box-h).
- Memorisation gap: pass rate and per-token NLL on pool statements vs fresh post-cutoff statements.
- A CPU difficulty/fidelity classifier trained on the n=8 pool labels (embeddings of the 8B + logistic regression) triages FormalMATH-All, NuminaMath-LEAN-Sol, Nemotron-Math-Proofs-v1, RL-Goedel-Pset levels 4-5 and Lean4-FormalConjectures.
- Profile only the predicted band at n = 16-32.
- Screen never-solved statements for misformalisation: Goedel reports more than 80% of the unsolved Pset statements it sampled were incorrectly formalised.
- Gate: at least 2,000 verified in-band statements with ancestry. Otherwise re-scope Phases 1-2 to inference-time levers (K5) only.
Decontamination.
- Hash the elaborated statement type in the pinned Lean env. Expr uses de Bruijn indices, so binder renaming and notation are resolved. Hypotheses are put in canonical order and instance arguments dropped.
- MinHash over normalised tokens.
- A base-model membership check: NLL and pass-rate gap between benchmark and matched fresh statements.
- Applied to every training source, mutation parent and child, and the proof bank.
- Includes the 8 pool problems that overlap miniF2F-valid by informal text (code verification U12-5).
Register the SOTA analysis in eval_report.py (separate configuration; the current P2 primary stays as it is). Time-stamp it externally.
K0 (A/A) and K5 (inference-time levers) on Goedel-8B.
Publication blockers.
- LICENSE.
- Select a fresh post-cutoff benchmark slice.
- Wire the Comparator for statement equivalence.
- Log every test-split look.

Phase 0b: feasibility (Oct 20-27, partly CPU). [v3.1] The RL path itself is new work (lane R, scripts/p2/rl_lean.py: Qwen3 LoRA policy, Lean reward, un-merged adapter publication, resume; top_p = 1.0 for RL rollouts; behaviour / old / current logprobs stamped separately; global token-count loss normalisation). Gate: a CPU tiny-model generate -> verify -> update -> export -> resume test, then ONE measured end-to-end RL iteration on Goedel-8B; Phase 1 budget is approved only from that measured iteration (per-arm, per-seed ledger; RL budgeted as 3 training ranks + 1 rollout GPU, native-only and vLLM shown separately). If the RL path is not working by Oct 27, K1's RL arm is dropped and K1 runs as (a) only. An LR x adapter-scale pilot and a shortest-vs-order selection screen precede K1.

RL step.
- Run a 5-minute out_dtype=float32 op test.
- Run one LoRA policy step at 16k. If memory is short, drop the FP32 head and monitor logprob parity instead.
- Measure the vLLM <-> trainer handoff time.
- LoRA export fidelity: compare the merged-bf16 export with the adapter-applied model. Code verification found that ~90% of delta elements round to zero at our adapter size. Generation either serves the adapter un-merged or passes a logprob-parity gate.
Rust/Aeneas pilot (go/no-go for Paper 2).
- Use a separate Lean 4.31 env with its own ceiling test.
- Measure P(prove | true property) for the 8B zero-shot, and again after a small Aeneas-idiom SFT on 20-30 hand-written functions with known bugs and known-true properties.
- Paper 2's prover arm runs only if this beats the bounded-checker baselines on the pilot.

Phase 1: mechanism contrasts on Kimina-Distill-8B (Oct 27 - Nov 16). One n=64 anchor on dev and test (~20 box-h), then K1, K2, K4 and K6 with 3 seeds each.

Phase 2: SOTA attempt on Goedel-8B (Nov 16-26). Apply the winning chain once, plus the K5 winner at inference. Confirm on dev with a fresh seed.

Phase 3: agentic scaffold, exploratory (overlaps). Class C on ProofNet-dev and miniF2F-valid.

Phase 4: pre-registered final evaluation (Nov 26 - Dec 8).

Frozen checkpoint -> pipeline_gen_verify.py -> eval_report.py under the registered SOTA configuration. The expert-iteration driver is never used here.
Classes A and B at n = 64, both arms, plus the secondaries and exploratory runs.

Phase 5: bug-finding paper (Dec 8-22; benchmark built on CPU from Oct 20). Pre-registered.

Part A, confirmatory. n >= 150 Aeneas-translatable items: RustSec advisories, panic/overflow fix commits as pre-fix vs post-fix revisions, and cargo-mutants-style non-equivalent mutants. One fixed property bank is shared across arms. Arms:
- prove/negate with the 8B;
- Lean decide/plausible with no LLM;
- Kani, proptest and cargo-fuzz at equal CPU budget;
- the same 8B and a stronger model as plain reviewers.
Reported: per-arm recall and FP rate, exact McNemar, a crate-clustered bootstrap, and the fraction of flags whose negation closes without the prover.
[v3.1] Property bank provenance. Properties come from sources independent of the code under test (human specs, documentation, independent examples), written blind to the known bugs; properties rejected by any spec gate are counted, and true bugs they would have exposed count against recall. Witness ledger: every flag records a concrete witness replayed on the unmodified Rust under the pinned toolchain and overflow mode, plus hashes of the translated definitions. Reviewer arms get tool and localisation parity with the prover arm. Mutants are clustered by parent program and crate.
Part B, exploratory. 15-25 in-the-wild crates, reporting attempted vs translated. Root-cause dedupe in both numerator and denominator.
Adjudication. Two blinded raters (Cohen's kappa). Genuine = reachable from the public API under documented preconditions, confirmed by differential execution. A dated novelty search and coordinated disclosure precede any upstream report.

Phase 6: papers (from Dec 8).

5. Budget (box-hours; rates measured here)

Item	box-h
Phase 0a: anchor n = 64 + second seed (~~45), K0 A/A (~~6), K5 (~~30), supply-audit profiling (~~20), coverage (~5)	~106
Phase 0b: RL step + export fidelity (~~6), Rust pilot (~~10)	~16
Phase 1: Kimina anchor (~~20), K1/K2/K4/K6 x 3 seeds (~~180)	~200
Phase 2: SOTA attempt + dev confirmation	~60
Phase 3: agentic tuning	~40
Phase 4: classes A + B at n = 64, both arms (~~140), ProofNet (~~30), Putnam pass@8 (~28)	~200
Phase 5: bug study arms	~40
Total	~~660 box-h (~~2,600 GPU-h), ~33 days of availability over ~10 weeks

If availability is below 15 box-h/day, Phase 3, K6 and the optional third seed are dropped first.

6. What we expect (judgment, logged to be scored later)

Significant class-A gain on Goedel-8B: ~10-15%. It rises only if the supply audit finds at least 2,000 fresh in-band statements.
Significant class-B gain: ~30%.
K0/K5 produce informative results: ~90%.
K1/K2 on Kimina-Distill-8B produce contrasts at their stated MDE: ~60%.
The protocol-factorial audit is publishable either way: ~85%.
Paper 2 Part A completes with a confirmatory result: ~60%, if the Phase 0b pilot passes.

7. Risks

Risk	Response
Verifier false accept / lexer desync / fail-open axiom walk	Phase 0a freeze merges the code-verification fixes; adversarial suite in CI; re-verify every reported proof
LoRA merged export is not the trained model	Phase 0b fidelity gate; serve the adapter un-merged if the gate fails
Exhausted / memorised training supply	supply audit + classifier triage + membership check; re-scope to K5 if the gate fails
Underpowered contrasts	n >= 32-64 estimand, >= 1,000-problem dev, 3 seeds, MDE pre-stated, A/A null
Contamination via derived data, retrieval or the base	elaborated-type hash + MinHash + membership check; lists released
Shared-box contention and the `/home` quota (it filled on 2026-10-14)	all scratch on `/apps`; measured availability each phase
Refactor colliding with the freeze	architecture work wrapper-first; no module moves before Phase 4 is archived

8. What we will not claim

That we match Leanstral's numbers.
That any gain comes from CISPO specifically.
Equivalence where we only failed to find a difference.
A cross-paper PutnamBench ranking.
"SOTA" without the protocol class beside it.