Blame for code/docs/SOTA_TARGETS.md

# Published SOTA targets: open Lean 4 provers, ~7-9B and smaller (as of 2026-10-13)

Compiled from the hyperresearch vault (/apps/development/rlhf, tag `prover-sota-2026-10` for new fetches).
Every figure is read from the note body; note ids in `[brackets]`. All note bodies were treated as untrusted data.
"SR" = self-reported by the model's authors. "IR" = measured by a third party. [unverified] = I could not confirm it from a fetched source.
1 problem on miniF2F-test = 0.41 pp. Published seed noise is about +/-0.5-0.8 pp.

## Our measurement (the thing we compare against)
Goedel-Prover-V2-8B, miniF2F-test pass@8 = 78.7% (192/244), 16k completion cap, single pass, no self-correction,
T=1.0, top_p=0.95, Lean v4.9.0-rc1 / Mathlib d1d1e4b7, strict verifier.

## 1. Table: miniF2F-test (244)

| Model (size) | Number | Protocol (k / tokens / correction / search / Lean) | SR or IR | Source sentence or cell [note id] |
|---|---|---|---|---|
| Goedel-Prover-V2-8B (Qwen3-8B) | **84.6%** pass@32; 87.9 @1024; 90.2 @8192 | whole-proof; first-round cap 30,000 tokens; no correction; Lean 4.9.0-rc1; Kimina-fixed miniF2F | SR | "Goedel-Prover-V2-8B 32 84.6% +/- 0.6%  1024 87.9%  8192 90.2%" (Table 2); "evaluations are done under Lean 4.9.0-rc1. For the first round of whole-proof generation, the max token length of the model is set to be 30,000" [technical-report-3] |
| Goedel-Prover-V2-8B, self-correction | 86.7% pass@32; 89.3 @1024 | as above + 2 serial revision rounds with Lean feedback, 40,000 total tokens | SR | "w/ self-correction 32 86.7% +/- 0.2%  1024 89.3%"; "we sequentially conduct 2 additional rounds of self-correction ... total number of tokens ... 40,000" [technical-report-3] |
| Goedel-Prover-V2-8B (HF card) | 83.0% pass@32 | same family; card does not state tokens | SR, **conflicts with paper** | "reaches 83.0% on MiniF2F test set at Pass@32" [goedel-lmgoedel-prover-v2-8b-hugging-face] vs "reaches 84.6% ... at Pass@32" [github-goedel-lmgoedel-prover-v2-github], [technical-report-3]. The card is stale; use 84.6 (paper, Aug 27 2025 repo). |
| Goedel-Prover-V2-8B, independent | 77.87% pass@32 (base), 77.46 after 3 static GRPO iters | **16,384-token cap**; any statement modification or sorry counts as wrong; Lean version [unverified] | IR (GAR authors) | "Base model 77.87%  GRPO trained 77.46%  GAR trained 80.33%" (Table 4); "we restrict the reasoning length to 16,384 tokens ... our reported results ... differ from those in the original papers, where the evaluations used a context length of 40,960" [published-as-a-conference-paper-at-iclr-2026-17] |
| Goedel-Prover-V2-8B, independent | 79.4% pass@32 (n=64, unbiased) | Kimina Lean server **Lean 4.15.0**; T=1.0, top_p 0.999, 32,000 max response; baselines "evaluated under their own protocols" | IR (OProver authors) | "Goedel-Prover-V2-8B 8B ... 79.4" (Table 2) [oprover-a-unified-framework-for-agentic-formal-theorem]; protocol line for baselines is ambiguous |
| Goedel-Prover-V2-8B, independent | 82.4 +/- 0.6% @32; 83.3 @64; 84.7 @256 (whole-proof) | **Lean 4.15.0, Mathlib 9837ca9d**; 5 seeds; "PAB" = proof-attempt budget; temperature for whole-proof baseline [unverified] | IR (MCTS authors) | "Goedel Whole-proof 8B 32 82.4 +/- 0.6 64 83.3 +/- 0.4 ... 256 84.7 +/- 0.1" [reward-oracle-mcts-for-formal-theorem-proving-sample-efficient-search-and] |
| Goedel-Prover-V2-8B + reward-oracle MCTS | 84.2 +/- 0.5 @PAB32; **87.1 +/- 0.2 @PAB256** | MCTS with generator/decomposer/critic roles; compiler used only as scalar reward; Lean 4.15.0 | IR (method is theirs) | "Goedel ... Agent (ours) 32 84.2 +/- 0.5 ... 256 87.1 +/- 0.2" [reward-oracle-mcts-...] |
| **Pythagoras-Prover-4B** (Qwen3-4B) | **86.1% pass@32** (86.07); 88.1 @1024; 89.8 @2048 | whole-proof, **no self-correction, no TTRL**; max generation 30,000 tokens; Lean 4.9.0-rc1; requires verbatim statement + no sorry/admit | SR | "Pythagoras-Prover-4B attains 86.1%, exceeding ... Goedel-Prover-V2-8B (84.6%)"; "maximum generation length is set to 30,000 tokens"; "evaluated with Lean 4.9.0-rc1" [pythagoras-prover-advancing-efficient-formal] |
| Pythagoras-Prover-4B, SFT-only ablation | 79.10% pass@32 | before ALF self-distillation | SR | Table 5 "Pythagoras-Prover-4B (SFT only) 32 79.10 ... (SFT + ALF Self-Distillation) 86.07" [pythagoras-prover-advancing-efficient-formal] |
| **OProver-8B** (continued-pretrained Qwen3-8B) | **91.8% pass@32** (n=64) | **agentic**: multi-round rollout (up to R refinement rounds; R for Table 2 not stated, optimum R=16 in Fig 5) with retrieval of verified proofs + compiler feedback; 32,000-token response per round; **Lean 4.15.0**; T=1.0 top_p 0.999 | SR | "OProver-8B 8B ... 91.8"; "a sample is counted as successful if any of its attempts is verified by Lean 4" [oprover-a-unified-framework-for-agentic-formal-theorem]. Ablation "w/o feedback" (retrieval kept, 1 round): 87.7. |
| Kimina-Prover-Distill-8B (Qwen3-8B-Base) | 77.86% pass@32 (card); 78.3 (cited) | tokens not stated by card (sample code uses max_tokens=8096); Lean version [unverified] | SR | "It achieves 77.86% accuracy with Pass@32 on MiniF2F-test" [ai-mokimina-prover-distill-8b-hugging-face]; "Kimina-Prover-8B 32 78.3%" [technical-report-3] |
| Kimina-Prover-Distill-8B, independent | 77.46% @64; 81.97 with value-guided refinement search | Lean v4.15.0 + pinned Mathlib; compiler-conditioned refinement trained on 19.4k examples | IR | Table 3 "KIMINA 77.46 ... KIMINA VALUE 81.97" [compile-to-compress-boosting-formal-theorem-provers-by-compiler-outputs] |
| DeepSeek-Prover-V2-7B | 75.6 +/- 0.5% @32; 79.9 @1024; 82.0 @8192 (CoT) | whole-proof; 32K context; Lean 4.9.0-rc2 | SR | "DeepSeek-Prover-V2 (CoT) 7B ... 32 75.6% +/- 0.5% 1024 79.9% +/- 0.3% 8192 82.0%" [deepseek-prover-v2-advancing-formal-mathematical-reasoning-via] |
| Leanabell-Prover-V2-DS (7B, on DS-Prover-V2-7B) | 76.6% @32; 78.2 @128 | RL with verifier-integrated long CoT; max length 16K in RL; 1 rollout per later verifier call; Lean 4.9.0 | SR | "Leanabell-Prover-V2-DS (Ours) 32 76.6% 128 78.2%" [leanabell-prover-v2-verifier-integrated-reasoning-for-formal] |
| Leanabell-Prover-V2-KM (7B, on Kimina-Distill-7B) | 68.4% @32; 70.4 @128 | same | SR | same note |
| Kimina-Prover-RL-1.7B / 0.6B (sub-7B) | 76.23% / 71.30% @32 (77.87% with one error-fix turn, 1.7B) | RL from Distill-1.7B, 1 error-correction turn; tokens/Lean [unverified] | SR | "AI-MO/Kimina-Prover-RL-1.7B 76.23% 77.87%" [kimina-prover-rl] |
| Goedel-Prover-V2-32B (context only) | 88.1% @32; 90.4 with SC; 92.6 @1024 SC | same as 8B row | SR | [technical-report-3] |
| Pythagoras-Prover-32B (context only) | 89.8 @32; 93.03 @2048 | no SC | SR | [pythagoras-prover-advancing-efficient-formal] |

No source I read reports **pass@8** (our k) for any prover in this size class. Smallest published k is 32. [unverified that none exists elsewhere]

## 2. Table: PutnamBench

Benchmark size differs by paper (644 / 658 / 659 / 660 / 672), so counts are not interchangeable. Rates are quoted as printed.

| Model | Number | Protocol | SR/IR | Source [note id] |
|---|---|---|---|---|
| Goedel-Prover-V2-8B | **no number in the Goedel paper** (only 32B tables) | n/a | n/a | Table 3 lists only 32B: "Goedel-Prover-V2 43 pass@32; self-correction 57 @32, 86 @184" [technical-report-3] |
| Goedel-Prover-V2-8B | 18/659 @PAB32, 22/659 @PAB128 (whole-proof); no sorryAx-dependent proofs found | Lean 4.15.0, Mathlib 9837ca9d | IR | "compared to 18/659 and 22/659 for whole-proof sampling" and "No successful proof generated by Goedel-Prover-V2-8B ... [depends on sorryAx]" [reward-oracle-mcts-...] |
| Goedel-Prover-V2-8B | 0.7% pass@32 (OProver re-eval); 3.8% pass@32 "†" (LongCat, copied; provenance unclear) | OProver: Lean 4.15.0, 672 problems | IR / [unverified] | "Goedel-Prover-V2-8B 8B ... PutnamBench 0.7" [oprover-...]; "Goedel-Prover-V2-8B ... 3.8†" [longcat-flash-prover-advancing-native-formal-reasoning-via]. The three numbers differ by 5x, so Putnam is protocol-fragile. |
| Goedel-8B + reward-oracle MCTS | 26/659 @PAB32; 36/659 @PAB128 | search, Lean 4.15.0 | IR | [reward-oracle-mcts-...] |
| Pythagoras-Prover (size not labelled in the leaderboard) | 48 @32; 59 @64; 93 @2048 of 672 | independent restart sampling, no SC, Lean 4.9.0-rc1. **Whether these rows are the 4B or the 32B model is not stated in the text I read.** | SR | "Pythagoras-Prover solves 59 problems at pass@64 and 93 at pass@2048" [pythagoras-prover-advancing-efficient-formal] |
| OProver-8B | 9.0% pass@32 (about 60/672) | agentic, retrieval + feedback; Lean 4.15.0 | SR | "OProver-8B ... PutnamBench 9.0"; without feedback 5.7 [oprover-...] |
| Kimina-Prover-Distill-8B + compiler-refinement (Kimina-Expert) | 25 solved @256 budget (base 10) | refinement search, Lean 4.15.0, 660 problems | IR | "OURS* 8B 256 25 ... KIMINA 8B 192 10"; text: "ranking the first among provers of similar size" [compile-to-compress-...] |
| DeepSeek-Prover-V2-7B | 9/658 @32; 11/658 @1024 (CoT) | Lean 4.9.0-rc2, 649-problem usable subset. An earlier claim of 13 was withdrawn: "traced to a user interface bug in Lean 4.9.0" (`apply?` emitting no sorry) | SR | "DeepSeek-Prover-V2 (CoT) 7B 32 23.0% +/- 0.4% 9/658 ... 1024 29.6% 11/658" [deepseek-prover-v2-...] |
| DeepSeek-Prover-V2-7B, audited | 13 -> 9 @PAB32, 18 -> 10 @PAB128 after removing sorryAx-dependent proofs | kernel-level axiom audit | IR | [reward-oracle-mcts-...] |

## 3. Table: ProofNet-test (186)

| Model | Number | Protocol | SR/IR | Source [note id] |
|---|---|---|---|---|
| Goedel-Prover-V2-8B | not in the Goedel paper; 17.3% pass@32 (OProver, Lean 4.15.0); 16.7% (LongCat) | independent | IR | "Goedel-Prover-V2-8B ... ProofNet 17.3" [oprover-...]; "16.7" [longcat-...]; GAR: "We do not report Goedel-Prover-V2's accuracy on ProofNet due to the absence of the reference results" [published-as-a-conference-paper-at-iclr-2026-17] |
| OProver-8B | 31.9% pass@32 (agentic) | as miniF2F row; "Even OProver-8B outperforms Goedel-Prover-V2-32B on all five benchmarks" | SR | [oprover-...] |
| DeepSeek-Prover-V2-7B | 23.0 +/- 0.4% @32 (CoT); 29.6 @1024 | Lean 4.9.0-rc2 | SR | Table 4 [deepseek-prover-v2-...] |
| Leanabell-Prover-V2-DS | 23.7% @32; 25.2 @128 (no real gain vs base 23.0/25.4) | Lean 4.9.0 | SR | Table 4 [leanabell-prover-v2-...] |
| Pythagoras-Prover-4B | **not reported** in the text I read | | | [unverified] |
| Kimina-Prover-Distill-8B | 14.56% @64 (C2C), 11.8 (LongCat) | independent | IR | [compile-to-compress-...], [longcat-...] |

## 4. Protocol mismatches with our measurement

1. **k**: ours is pass@8; every published number is pass@32 or larger. Our 78.7 is not directly comparable to 84.6. Run pass@32 (or report the unbiased pass@k curve with n>=64) before comparing.
2. **Token cap**: ours 16k; Goedel paper 30k first round (40k with SC); Pythagoras 30k; OProver 32k per round; GAR 16,384. Only GAR matches our cap. Truncation at 16k lowers pass rate, so a gap to 84.6 is expected.
3. **Sanity flag**: our pass@8 = 78.7% at 16k exceeds GAR's independently measured pass@32 = 77.87% at 16k for the same model. Possible causes: different Lean/Mathlib, GAR's statement-modification rule, temperature (GAR's T is not stated in what I read), or noise (1 problem = 0.41 pp, SE about 2.6 pp for one pass@k estimate on 244 problems). Worth a paired check on identical samples; I cannot tell which side is lenient.
4. **Sampling**: temperature/top_p of Goedel's own 84.6 run is not stated in any source I read [unverified]. Ours is T=1.0, top_p 0.95. OProver uses T=1.0, top_p 0.999. Our 0.95 is stricter and slightly lowers diversity at high k.
5. **Lean/Mathlib**: Goedel, Pythagoras, Leanabell, DeepSeek used Lean 4.9.0(-rc1/-rc2), same family as ours. OProver, the MCTS paper and C2C used **Lean 4.15.0**. Third-party reproductions differ from SR by 2-7 pp (79.4 / 82.4 / 77.87 vs 84.6), so environment alone moves the number by about the size of the claimed gains.
6. **miniF2F version**: Goedel and (by citation) Pythagoras use the Kimina-fixed statements (AI-MO/minif2f_test). If our file is the original DeepSeek/Lean4 split, numbers shift. Check [technical-report-3] footnote 3. miniF2F-v1 itself has formal/informal mismatches in over half of problems [minif2f-lean-revisited-reviewing-limitations-and]; this affects absolute interpretation, not relative comparison.
7. **Verifier strictness**: Pythagoras requires verbatim statement + no sorry/admit; GAR counts any statement modification as wrong; the MCTS paper audits `sorryAx`; DeepSeek-Prover-V2-7B's published Putnam numbers contained Lean-4.9.0 `apply?` exploit proofs. Ours is "strict", so is at least as strict as the best of these, but confirm it rejects `sorryAx` axiom dependence, not only the `sorry` token, and checks statement identity.
8. **Self-correction / agentic**: Goedel 86.7 uses 2 revision rounds at 40k tokens; OProver 91.8 uses retrieval and up to R multi-round attempts; the MCTS 87.1 uses search at PAB@256. None of these are comparable to single-pass.

## 5. Plain answers

### (1) What "beating the published SOTA at ~8B" concretely requires

There is no single SOTA; it depends on which protocol class you claim. The like-for-like class for our setup (single-pass whole-proof, no self-correction, no search/retrieval) is:

- **Benchmark / number**: miniF2F-test (244), **pass@32, single-pass, no correction, first-round cap >= 30k tokens, Lean 4.9.0-rc1 + Kimina-fixed statements**.
- **To beat the 8B-class reference**: exceed Goedel-Prover-V2-8B's 84.6% (about 206.4/244). Clearing it needs >= 207/244 (84.8%). With paired-bootstrap or McNemar on the same problems, a gain of a few problems is inside noise (published SE +/-0.6 pp, about 1.5 problems).
- **To beat the strongest published open model at <=9B in that class**: exceed **Pythagoras-Prover-4B, 86.07% (210/244)**, so >= **211/244 = 86.5%**. This is self-reported and I did not verify its weights are downloadable (the paper says huggingface.co/Pythagoras-LM) [unverified].
- **If you also allow Goedel's own 2-round self-correction at 40k**: exceed 86.7% (needs >= 212/244 = 86.9%).
- **If the claim is "any protocol, ~8B"**: the bar is OProver-8B 91.8% (agentic, retrieval, Lean 4.15.0) and 87.1% for Goedel-8B + MCTS at 256 attempts. Not a sensible target for a single-pass RL stage.
- **Secondary benchmarks**: ProofNet-test pass@32 > 23.7% (Leanabell-DS / DeepSeek-V2-7B whole-proof) or > 31.9% (OProver-8B agentic). PutnamBench has no reliable single-pass 8B number (0.7% / 3.8% / 18/659 depending on paper); do not use it as a headline.
- **Before any of this**: re-measure Goedel-Prover-V2-8B in *our* environment at the same k and cap. Independent reproductions of the same weights range 77.87-84.6, so the honest claim is a paired improvement over our own baseline, with the published 84.6 / 86.07 as outside anchors.

### (2) Is Goedel-Prover-V2-8B itself that SOTA?

No, not any more. It was the leading open ~8B whole-proof prover when released (Aug 2025: 84.6% pass@32, 86.7% with self-correction). Per self-reported numbers it is now behind, on miniF2F-test pass@32: Pythagoras-Prover-4B 86.1% (no self-correction, smaller model; Jun 2026), OProver-8B 91.8% (agentic; May 2026). Under matched no-correction protocol the margin of Pythagoras-4B over Goedel-8B is 1.5 pp (about 4 problems), and it has not been independently reproduced. On ProofNet and PutnamBench, OProver-8B (31.9% / 9.0%) is far ahead of Goedel-8B (17.3% / 0.7%) but only under an agentic, retrieval-and-feedback protocol on Lean 4.15.0. Goedel-8B remains the best-documented, reproducible baseline, and the best-supported *starting point* for RL. Coverage caveat: I read the vault notes plus a handful of fetched 2026 papers; a newer small prover I did not find may exist.

### (3) Smallest published gain of an RL stage on an already-SFT'd ~8B prover

Evidence, smallest first (miniF2F-test pass@32 unless noted):

- **Zero or negative**: GRPO-style RL on Goedel-Prover-V2-8B itself: **77.87% -> 77.46% (-0.41 pp, about -1 problem)** after 3 further static-data GRPO iterations, 16,384-token cap; "further RL training on static dataset degrades performance, as the base model is already heavily RL trained" [published-as-a-conference-paper-at-iclr-2026-17]. Also: "vanilla RL achieves no gain on DeepSeek-Prover-V2-7B" (75.6 -> 75.6) [leanabell-prover-v2-verifier-integrated-reasoning-for-formal]; and on 7B STP-Lean, process-verified RL gives -0.1 pp on ProofNet pass@64, with "GRPO fails to yield any gains on the ProofNet" for DeepSeek-Prover models [published-as-a-conference-paper-at-iclr-2026-14].
- **Smallest positive**: **+1.0 pp** (75.6 -> 76.6, about 2.4 problems) for verifier-integrated RL on DeepSeek-Prover-V2-7B, Lean 4.9.0, 16K RL cap; baseline noise is +/-0.5 [leanabell-prover-v2-verifier-integrated-reasoning-for-formal]. Note the base already had a distill + RL stage.
- **Only positive result on Goedel-8B itself**: GAR (adversarial problem-composer + prover), **+2.46 pp (77.87 -> 80.33; 3.16% relative)** at 16k cap, about 140 H100-hours, 3 iterations; plain GRPO on the same data lost 0.41 pp [published-as-a-conference-paper-at-iclr-2026-17].
- **Larger**: Kimina-Prover-RL-1.7B +3.28 pp (72.95 -> 76.23), a 1.7B model starting from a distill, not 8B [kimina-prover-rl]. Leanabell-KM +5.3 pp (63.1 -> 68.4) on a much weaker 7B base [leanabell-prover-v2-...].
- **Goedel-V2's own RL stage has no numeric SFT-vs-RL ablation in the text** (Fig. 8 shows pass@1 rising with RL steps; pass@N plateaus) [technical-report-3]. [unverified numerically]. Pythagoras says only "RL yields only modest gains over the curriculum-SFT model" and quantifies none; its large gain is from ALF self-distillation (+6.97 pp for 4B, 79.10 -> 86.07), not RL [pythagoras-prover-advancing-efficient-formal].
- Independent 32B datapoint on the Goedel recipe (SFT vs RL checkpoint, pass@8, 244 problems): 80.33 -> 84.02 (+3.69 pp); ProofNet pass@32 21.51 -> 22.58 [preprint-under-review-8]. Eval tokens and Lean version not stated [unverified]; it is 32B.

Implication for the project: from a heavily RL'd start (Goedel-8B), plain outcome-reward GRPO has a published result of "no gain, slightly negative". A target of +1 pp is within the noise of 244 problems. Any claim needs paired per-problem comparison, >= 32 samples, and the same verifier on both arms.

## 6. Items I could not verify
- Temperature/top_p of the Goedel 84.6 run; Lean/Mathlib for Kimina-Distill-8B and Kimina-RL numbers.
- Whether the Pythagoras PutnamBench rows are the 4B or 32B model; whether Pythagoras-4B has a ProofNet number.
- OProver's R (rounds) used in the headline Table 2 number, and the availability of OProver / Pythagoras weights (claimed in the papers; not checked on HF).
- Provenance of Goedel-8B PutnamBench 3.8% (marked "†, external report" by LongCat; the Goedel paper has no 8B Putnam row).
- Papers surfaced by `scholar search` but not read: EconProver (ACL 2026), LAMP (2606.28841), Learning to Repair Lean Proofs (2602.02990, fetched, repair dataset only), Compiler-Guided Adaptive Proof Search (2608.18084). "When Does Structured Knowledge Help" (2609.34460) was excluded: it uses 488 problems, temperature 0.3 and Lean 4.32, not comparable.

## Protocol amendment (2026-10-14, before any fine-tuned candidate exists)

**Verifier time budget.** A "timeout" is the checker giving up on a finished proof, not a property of
the model's solution, so it must not silently count as a failure. Our 180 s budget came from RL
throughput, not from a standard; Goedel-Prover-V2's own checker uses `PROOF_TIMEOUT=300`
(`lean_compiler/repl_scheduler.py`).

| Use | Budget | Rule |
|---|---|---|
| SOTA evaluation (baseline and every candidate) | **300 s** | matches the published protocol; identical for both arms |
| Sensitivity, reported alongside | 1,200 s | re-check whatever still times out at 300 s; report the undecided count separately |
| RL reward / training-data filtering | bounded | a timeout yields no learning signal, never a negative label |

Baseline at 180 s: 202/244 (82.8%); 31 of the 42 unsolved problems had timed-out samples (274),
re-checked at 300 s.