Lean theorem proving on MINIF2F 244 problems
84.02Pass@8GOEDEL-PROVER-V2-32B-RL
Evaluation Results
| Method | Links | |||
|---|---|---|---|---|
| GOEDEL-PROVER-V2-32B-RLCheckpoint Type=Post-RL checkpoint2026.04 | 84.02 | 87.7 | 0 | |
| Post-hoc Agentic SFTBase checkpoint=GOEDEL-PROVER-V2-32B-RL, Lean agentic SFT data size=1K2026.04 | 81.15 | 84.43 | 84.5 | |
| GOEDEL-PROVER-V2-32B-SFTCheckpoint Type=SFT checkpoint2026.04 | 80.33 | 84.02 | 0 | |
| Post-hoc Agentic SFTBase checkpoint=GOEDEL-PROVER-V2-32B-SFT, Lean agentic SFT data size=1K2026.04 | 79.92 | 82.79 | 83.2 | |
| Post-hoc Agentic SFTBase checkpoint=GOEDEL-PROVER-V2-32B-SFT, Lean agentic SFT data size=18K2026.04 | 79.92 | 85.25 | 74.5 | |
| Post-hoc Agentic SFTBase checkpoint=GOEDEL-PROVER-V2-32B-RL, Lean agentic SFT data size=18K2026.04 | 79.92 | 84.02 | 72.2 | |
| Post-hoc Agentic SFTBase checkpoint=GOEDEL-PROVER-V2-32B-RL, Lean agentic SFT data size=1002026.04 | 77.87 | 83.2 | 80.3 | |
| Post-hoc Agentic SFTBase checkpoint=GOEDEL-PROVER-V2-32B-SFT, Lean agentic SFT data size=1002026.04 | 77.46 | 81.97 | 78.5 | |
| QWEN3-32B2026.04 | 7.79 | 14.34 | 31.4 |