code/docs/PREREG_SOTA.md

Pre-registration: SOTA analysis, Lean prover paper (configuration sota-v1)

Status: REGISTERED v1, 2026-10-19 (signed off by the project owner). The hash is python scripts/p2/prereg_hash.py (sha256 over this text AND the analysis code: align/eval/paired.py, align/eval/proof_stats.py, scripts/p2/eval_report.py, scripts/p2/p2_common.py, scripts/p2/prereg_hash.py). It is time-stamped with OpenTimestamps (Bitcoin-anchored; only the hash leaves the machine): docs/evidence/prereg/ holds the hash file and its .ots proof, verifiable with ots verify. Every edit after registration changes the hash, which eval_report.py --config sota prints beside the registered one; changes are made only as numbered, separately time-stamped amendments (section 9). License of everything released: Apache-2.0 (data rows keep their source licenses; see NOTICE).

Specification: docs/SOTA_PLAN.md v3, sections 1, 3 and 5, Phase 0a item 6. This registration is SEPARATE from the P2 registration in docs/P2.md (miniF2F solved@8 at cap 16384, exact McNemar), which stays as it is and is not reinterpreted by anything below.

1. Question and estimand

Does the frozen candidate (the winning recipe chain applied once to Goedel-Prover-V2-8B, plus the K5 inference-time winner) solve more miniF2F-test problems than the Goedel-Prover-V2-8B anchor, under one frozen verifier and the same protocol?

Estimand, per class: the mean over the problems of the benchmark of the unbiased pass@32 estimate

pass@32_i = 1 - C(n - c_i, 32) / C(n, 32),    n = 64 samples (class A) or 64 trajectories (class B),

where c_i is the number of samples (trajectories) of problem i accepted by the verifier. It is computed in product form (align.eval.paired.pass_at_k_product, checked against math.comb). The estimand is the difference of these means, candidate minus anchor, over the same problems. k > n is refused, never extrapolated.

Classes (every number carries its class):

• A: single pass, cap 40,960 tokens, n = 64 samples per problem.
• B: one trajectory is an attempt plus at most 2 Lean-feedback repairs; the cumulative completion tokens of the trajectory may not exceed 40,960 (a success reached only after the ledger is exceeded does not count). n = 64 trajectories per problem. A failed sample with ledger left and no repair record is a missing record, and the report refuses it; it is never scored as a failure.
• C (agentic) and PutnamBench class A pass@8 are exploratory and not analysed by this configuration beyond what is listed in section 3.

2. Primary endpoints (co-primary, Holm over the two)

Id	Class	Set	Estimand	Test
A	A	miniF2F-test (the elaborating subset, fixed in Phase 0a)	mean unbiased pass@32 from n = 64	paired sign-flip permutation test over problems
B	B	miniF2F-test (same problems)	same	same

• Test. Statistic: the mean of the per-problem differences d_i. Null: d_i symmetric about 0 (exchangeability of the two systems within a problem). p = P(|mean(s * d)| >= |observed|) over independent uniform sign vectors s; zero differences are dropped from the enumeration. Exact enumeration of all 2^m sign vectors when at most 20 problems differ; otherwise Monte Carlo with 10^5 flips, seed 0, p = (count + 1) / (10^5 + 1). Two-sided.
• alpha = 0.05 two-sided, familywise over {A, B} by Holm step-down (valid under arbitrary dependence). An endpoint that cannot be computed enters Holm with p = 1 (the family is the registered two).
• Decision rule, applied mechanically: SUCCESS iff the Holm-adjusted p < 0.05 AND the candidate mean is higher; significant with the candidate lower is reported as DEGRADATION; anything else is "no detectable improvement" (never "no effect"; never "equivalent").
• Interval: 95% percentile bootstrap over problems (10^4 resamples) of the mean paired difference.
• Label. A result is CONFIRMATORY only if eval_report.py lists no blocker: the problem count equals the registered count; n per problem equals 64 in both arms; both arms were verified under the frozen verifier (section 7) at the registered 300 s budget with a single verifier configuration; the two arms' generation settings and prompts match; the registration hash matches the time-stamped one; statement fidelity was checked for every accepted sample; no override flag was used. Anything else prints NOT CONFIRMATORY with the reasons, and the numbers are exploratory.

3. Secondary and exploratory (no multiplicity control, no decision attached)

Secondary:

1. Exact McNemar on the binary solved@32 of the first 32 samples (by sample_idx) of class A.
2. Mean pass@1 (class A), same paired test and interval.
3. ProofNet-test class A, pass@32 estimand, same test (its own elaborating subset; reported with its denominator).

Exploratory: class-A pass@1/8/16 on miniF2F-test; every other (benchmark, split) supplied, class A at k in {1, 8, 16, 32}; the strict-fidelity sensitivity (rewritten or unreadable accepted samples counted as failures); anything on class C. If the strict-fidelity sensitivity reverses the sign or the significance of a co-primary, the headline is published with that reversal in the same sentence.

4. Minimum detectable effects

Power is by simulation (align.eval.paired.simulate_power / mde_curve; 400 to 5,000 simulations per point, seed 3). It is a statement about a stated difficulty distribution, not about a real benchmark: per-problem success probabilities drawn from the mixture of .tmp/audit_scratch/power_sim3.py (68% Beta(3, 1.5); 20% Beta(0.45, 5); 12% log-uniform on 10^-6 to 10^-3.2), and the candidate's log-odds shifted by mu plus problem-specific noise of sd 1. MDE = true gain in pass@k (pp) at which the linearly interpolated simulated power reaches 80%.

Reproduction check (N = 226, n = 32, k = 8, as in power_sim3.py): +1.4 pp gives power 0.28 (reference 0.30), and +3.6 pp gives 0.95 (reference 0.96), for the estimator test; binary McNemar gives 0.08 and 0.41 (reference 0.07 and 0.42). The estimator test needs about half the effect of binary McNemar for the same power.

Contrast (plan section 3)	Set, estimand	Difficulty assumed	MDE, estimator test (80%)	MDE, binary McNemar (80%)	Prior effect to beat (plan section 2)
Co-primary A and B	miniF2F-test, N = 244, pass@32 from n = 64	Goedel-like mixture above	2.8 pp (about 6.7 problems)	not reached below +3.8 pp	descriptive target: >= 207 of 244
K0 A/A null	dev, N >= 1,000, pass@8 from n = 32	Goedel-like	not a test: supplies the null spread of paired differences between two identical-recipe seeds		0
K5 inference levers	dev, N >= 1,000, pass@8 from n = 32	Goedel-like	1.3 pp	2.5 pp	L1: +2.1 (SR, same model)
K1 EI-SFT vs RL (+PKPO arm)	dev, N >= 1,000, pass@8 from n = 32	headroom (log-odds shifted by -1)	1.7 pp	3.1 pp	L3: 0 to +2.5; L5: +1.8 to +2.8
K2 mutation vs temperature-matched	same	headroom	1.7 pp	3.1 pp	0 to +3.0 pp (Pythagoras ALF +6.97 pp at 4B with ~2M instances; ours ~100x smaller; judgment)
K4 averaging / scale	same, per arm at its own validated alpha	headroom	1.7 pp	3.1 pp	0 to +2.0 pp at the best validated alpha vs alpha = 1.0 (Goedel-V2 averaging: pass@N rises then falls with alpha; judgment); curves reported
K6 classifier vs random statements	same, 0.1B tokens	headroom	1.7 pp	3.1 pp	0 to +1.0 pp (text-feature classifier held-out AUC 0.52: no signal); conditional: if the 8B hidden-state classifier reaches held-out in-band AUC >= 0.65 (measured before K6 data are built), the prior is 0 to +2.0 pp

Rules attached to the table:

• A contrast whose MDE exceeds the upper end of its prior effect is dropped, not run (plan section 3). By this rule K1 (1.7 < 2.5), K2 (1.7 < 3.0) and K4 (1.7 < 2.0) are run; K6 (1.7 > 1.0) is DROPPED unless its pre-stated condition (hidden-state AUC >= 0.65) is met, in which case it runs (1.7 < 2.0). The rule is re-applied with the recomputed MDEs of Amendment A1.
• Amendment A1 (scheduled): the table is recomputed with the anchor's own per-problem (n, c) table at n = 64 (align.eval.paired.empirical_difficulty) and the actual dev N, and the co-primary n_problems is set to the final elaborating subset. A1 uses baseline data only, is time-stamped like v1, and must exist BEFORE any contrast or candidate result is computed. MDEs scale roughly with 1 / sqrt(N).
• These MDEs cover benchmark-sampling noise only. Training-seed noise is added by design in section 5.
• Dev-set size: at least 1,000 problems (plan section 3: held-out in-band pool statements with labelling samples disjoint from the selection samples, plus ProofNet-dev, plus miniF2F-valid (226, filtered, disclosed)). Fewer problems means the MDE is re-stated, not ignored.

5. Contrasts K0 to K6: analysis (decided on the dev set at matched generated tokens)

• The unit is the problem. Per arm, the per-problem estimate is the mean over training seeds (at least 3) of the unbiased pass@k estimate; arms are compared with the same paired sign-flip test and bootstrap interval as section 2.
• A K-contrast headline requires BOTH: Holm-adjusted p < 0.05 within its family, AND the observed paired difference exceeds the 97.5th percentile of the K0 null distribution of paired differences (two seeds of the identical recipe), so training-seed noise cannot pass as an effect. Families: {K1, K2, K4, K6} (mechanism contrasts on Kimina-Distill-8B, one Holm family); K5's pairwise comparisons (2-repair vs restarts vs agentic) another. K0 is a calibration, not a test.
• Contrasts use the registered code path (sota_contrast); nothing is tuned on the dev set after its first read except the K4 alpha, which is selected per arm on the dev half disjoint from the confirmation half.
• No contrast may be described as equivalence (we claim only failure to detect a difference at its MDE).

6. Anchor

The anchor is Goedel-Prover-V2-8B at the revision dfd02e6271a58375dfbf3ece0175277cf6b6a89a (the revision pinned in scripts/p2/eval_report.py for the P2 registration). In Phase 0a it is re-generated at n = 64 (cap 40,960, the P2 sampling settings temperature 1.0 / top_p 0.95, no top_k) and re-verified under the frozen verifier at 300 s; a sensitivity run at 1,200 s is reported separately and never pooled. A second seed of the generation is run to measure generation variability. The published self-reported 202 of 244 (pass@32, 40k, 180 s) is context, not the anchor: the anchor is our own n = 64 regeneration, and every comparison uses the baseline and the candidate under the same harness, sampler settings and prompts.

Class B's anchor is the same model run through the same repair protocol (2 Lean-feedback repairs, 40,960 cumulative tokens).

7. Frozen-verifier rule

Before any candidate result exists, the verifier (everything under align/verify/, the Lean and Mathlib pins, the axiom policy, timeouts) is merged, ceiling-tested (known-good accepted, the adversarial suite rejected) and frozen. Its hash is verifier_hash of eval_report.py (sha256 of the canonical JSON of the recorded pins and configuration, workers excluded). All arms of every confirmatory comparison are verified under that one verifier, passed as --frozen-verifier-hash. A verifier fix after the freeze invalidates every confirmatory number produced before it: the anchor and candidate are both re-verified, never mixed. Re-verifying the same generations is allowed and does not consume a test look; generating anew does.

8. Rewritten statements

The verifier replaces the statement the model wrote with the reference statement, so a sample whose displayed theorem differs from the reference can be accepted. The Goedel protocol credits these, and so does the primary analysis (comparability). Every report states, per arm, the rewritten-statement count: accepted samples whose displayed theorem (signature tokens, theorem name ignored) differs from the reference statement or cannot be parsed, with the number of affected problems and how many fall in repair rounds. The strict-fidelity sensitivity (section 3) is the exploratory counterpart.

9. Stopping and exclusion rules

• One confirmatory look at the test split per frozen candidate. No interim analysis, no optional stopping, no peeking: n = 64 is fixed in advance.
• Every look at a test split is appended to docs/evidence/test_split_looks.jsonl (who, when, which files and sha256 of the report and inputs; hash-chained, verifiable with verify_look_log). A look not in the log did not happen.
• A generation job that dies is re-run for the missing shard under the same seed settings. A problem or sample is never dropped for having failed. An incomplete run (missing round-0 sample, missing verification, ragged n) makes the report refuse, not score the gap as failure.
• Exclusions are only the pre-declared ones: problems that do not elaborate under the frozen Lean environment are excluded as a set, fixed in Phase 0a before any candidate result and disclosed with the denominator; the registered n_problems in eval_report.SOTA must equal that denominator at hash time. No other exclusion, and no outlier trimming, ever.
• If any registered input changes (denominator, n, cap, verifier, test), the registration is re-hashed and re-stamped and the earlier results lose the label.

10. Protocol tuple

Every reported number carries: benchmark and split; denominator; sha256 of the (problem id, statement hash) set; Lean and Mathlib pins; verifier hash, budget and configuration (axiom policy); the rewritten-statement count per arm; n, k, cap, ledger and total completion tokens; class. "SOTA" is never claimed without the class beside it. Cost (box-hours, decode/prefill tokens, verifier CPU-hours) is reported from the run logs alongside.

11. What this registration does not claim

That we match Leanstral's numbers; that any gain comes from a specific objective; equivalence where only a difference was not detected; a cross-paper PutnamBench ranking; that the MDEs describe the real benchmark rather than the stated difficulty distribution.

9. Amendments

Each amendment is appended here with its date, its reason, the hash before and after, and its own OpenTimestamps proof. None yet (A1 is scheduled, see section 4).