Formal Theorem Proving on MiniF2F (test)
100Pass@1Goedel-Architect
Evaluation results
| Method | Links | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Goedel-ArchitectNatural language guidance (+NL)=true2026.06 | 100 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Seed Prover2025.09 | 99.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Seed-Prover2026.06 | 99.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| HILBERTcritic_model=Gemini 2.5 Pro, prover_model=Goedel-Prover-V2-32B2025.09 | 99.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Hilbert2026.06 | 99.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-ArchitectNumber of samples (k)=1, Natural language guidance (+NL)=false2026.06 | 99.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| HILBERTcritic_model=Gemini 2.5 Pro, prover_model=DS Prover-V2-7B (non-CoT)2025.09 | 98.4 | — | — | — | — | — | — | — | — | — | — | — | — | |
| LongCat-Flash-ProverNumber of samples (k)=722026.06 | 97.1 | — | — | — | — | — | — | — | — | — | — | — | — | |
| HILBERTcritic_model=Gemini 2.5 Flash, prover_model=DS Prover-V2-7B (non-CoT)2025.09 | 96.7 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Delta Proversampling_budget=pass@163842025.09 | 95.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| BFS-Prover-V2-32B w/Planner2025.09 | 95.1 | — | — | — | — | — | — | — | — | — | — | — | — | |
| HILBERTcritic_model=Gemini 2.5 Flash, prover_model=Goedel-Prover-V2-32B2025.09 | 94.7 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-V2-32Bself-correction=true, sampling_budget=pass@10242025.09 | 92.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-V2Number of samples (k)=10242026.06 | 92.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| ProofSketcher2026.04 | 92.21 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-72Bsampling_budget=pass@1024, TTRL=true2025.09 | 92.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-V2-32Bsampling_budget=pass@81922025.09 | 92.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| HILBERTcritic_model=gpt-oss-120b, prover_model=Goedel-Prover-V2-32B2025.09 | 90.8 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-V2-8Bsampling_budget=pass@81922025.09 | 90.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-V2-8Bself-correction=true, sampling_budget=pass@10242025.09 | 89.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V22026.04 | 88.93 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V2-671Bsampling_budget=pass@81922025.09 | 88.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-V2Regime=Fine-tuned on Lean traces2026.06 | 88.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-72Bsampling_budget=pass@10242025.09 | 87.7 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V2-7B (CoT)sampling_budget=pass@81922025.09 | 82 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-PreviewProver system type=Whole-proof, Model size=72B, Sample budget=81922025.04 | 80.74 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-PreviewSample budget=81922025.04 | 80.74 | — | — | 40 | 86.67 | — | — | — | — | — | — | — | — | |
| Kimina-Prover-8Bsampling_budget=pass@322025.09 | 78.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-PreviewProver system type=Whole-proof, Model size=72B, Sample budget=10242025.04 | 77.87 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V2-7B (non CoT)sampling_budget=pass@81922025.09 | 75 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-V2-32Bsampling_budget=pass@42025.09 | 74.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| BFS-ProverProver system type=Tree search, Model size=7B, Sample budget=2048 × 2 × 6002025.04 | 70.8 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-Preview-Distill-7BProver system type=Whole-proof, Model size=7B, Sample budget=10242025.04 | 70.8 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-PreviewProver system type=Whole-proof, Model size=72B, Sample budget=322025.04 | 68.85 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-PreviewSample budget=322025.04 | 68.85 | — | — | 20 | 46.67 | — | — | — | — | — | — | — | — | |
| HunyuanProver v16+BFS+DCProver system type=Tree search, Model size=7B, Sample budget=600 × 8 × 4002025.04 | 68.4 | — | — | — | — | — | — | — | — | — | — | — | — | |
| STPsampling_budget=pass@256002025.09 | 67.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| CoR-Math-7BSample Budget N=128×1282025.01 | 66 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM2.5-StepProver-BF+CGSample Budget N=256×32×6002025.01 | 65.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM2.5-StepProver-BF+CGProver system type=Tree search, Model size=7B, Sample budget=256 × 32 × 6002025.04 | 65.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM-StepProverRegime=Fine-tuned on Lean traces2026.06 | 65.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-PreviewProver system type=Whole-proof, Model size=72B, Sample budget=82025.04 | 65.16 | — | — | — | — | — | — | — | — | — | — | — | — | |
| STPsampling_budget=pass@32002025.09 | 65 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-SFTProver system type=Whole-proof, Model size=7B, Sample budget=256002025.04 | 64.7 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RL + RMaxTSSample Budget N=32×64002025.01 | 63.5 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RL + RMaxTSProver system type=Tree search, Model size=7B, Sample budget=32 × 16 × 4002025.04 | 63.5 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-Preview-Distill-7BProver system type=Whole-proof, Model size=7B, Sample budget=322025.04 | 63.1 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-SFTsampling_budget=pass@32002025.09 | 62.7 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-Preview-Distill-1.5BProver system type=Whole-proof, Model size=1.5B, Sample budget=10242025.04 | 61.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V2-7B (non CoT)sampling_budget=pass@42025.09 | 61.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Leanabell-ProverProver system type=Whole-proof, Model size=7B, Sample budget=1282025.04 | 61.1 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-SFT + RMaxTSSample Budget N=32×64002025.01 | 60.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RLProver system type=Whole-proof, Model size=7B, Sample budget=1024002025.04 | 60.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RL + RMaxTSSample Budget N=4×64002025.01 | 59.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM2.5-StepProver-BFSample Budget N=256×32×6002025.01 | 59.4 | — | — | — | — | — | — | — | — | — | — | — | — | |
| STP-Lean + OursModel size=7B, Budget=642026.06 | 59.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM2.5-StepProverModel size=7B, Budget=4 × 32 × 6002026.06 | 58.5 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-SFTModel size=7B, Budget=642026.06 | 57.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5 + STP + OursModel size=7B, Budget=642026.06 | 57.8 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5 + STPModel size=7B, Budget=642026.06 | 57.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| STP-Lean + OursModel size=7B, Budget=322026.06 | 57.1 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Goedel-Prover-SFTModel size=7B, Budget=322026.06 | 56.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| STP-LeanModel size=7B, Budget=642026.06 | 56.7 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-SFT + RMaxTSSample Budget N=4×64002025.01 | 56.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5 + STP + OursModel size=7B, Budget=322026.06 | 56.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-Preview-Distill-1.5BProver system type=Whole-proof, Model size=1.5B, Sample budget=322025.04 | 56.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| SubgoalXLBase model=Llama-3-8B, Use human-written informal proofs=true2024.08 | 56.1 | — | — | — | — | — | — | — | — | — | — | — | — | |
| STP-LeanModel size=7B, Budget=322026.06 | 55.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RL + RMaxTSModel size=7B, Budget=3,2002026.06 | 55 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5 + STPModel size=7B, Budget=322026.06 | 54.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM2.5-StepProverSample Budget N=64×32×1002025.01 | 54.5 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-PreviewProver system type=Whole-proof, Model size=72B, Sample budget=12025.04 | 52.94 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-Preview-Distill-7BProver system type=Whole-proof, Model size=7B, Sample budget=12025.04 | 52.5 | — | — | — | — | — | — | — | — | — | — | — | — | |
| LyraBase model=GPT-4, Use human-written informal proofs=true2024.08 | 51.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM2.5-StepProver-BF+CGSample Budget N=2×32×6002025.01 | 50.7 | — | — | — | — | — | — | — | — | — | — | — | — | |
| LEGO-ProverBase model=GPT-3.5-Turbo, Use human-written informal proofs=true2024.08 | 50 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover2026.04 | 50 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Gemini 2.5 Prosampling_budget=pass@163842025.09 | 49.1 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RLModel size=7B, Budget=642026.06 | 48.8 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM2-Math-Plus-7BModel size=7B, Budget=1 × 32 × 1002026.06 | 48.8 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RLModel size=7B, Budget=322026.06 | 48 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-SFTModel size=7B, Budget=642026.06 | 47.5 | — | — | — | — | — | — | — | — | — | — | — | — | |
| InternLM2.5-StepProver-BFSample Budget N=1×32×6002025.01 | 47.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Lean-STaRSample Budget N=64×1×502025.01 | 46.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Lean-STaRModel size=7B, Budget=64 × 1 × 502026.06 | 46.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-SFTModel size=7B, Budget=322026.06 | 46.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Subgoal-ProverBase model=GPT-3.5-Turbo, Use human-written informal proofs=false2024.08 | 45.5 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Kimina-Prover-Preview-Distill-1.5BProver system type=Whole-proof, Model size=1.5B, Sample budget=12025.04 | 42.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-BaseSample Budget N=64002025.01 | 42.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| POETRYenvironment=Isabelle2024.05 | 42.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Hypertree Proof SearchSample Budget N=64×50002025.01 | 41 | — | — | — | — | — | — | — | — | — | — | — | — | |
| VERITASRegime=Zero-shot, inference-only2026.06 | 40.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| DSPBase model=Codex, Use human-written informal proofs=true2024.08 | 39.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| ReProver*Model detail=newly provided pre-trained model2025.03 | 37.7 | — | — | — | — | — | — | — | — | — | — | — | — | |
| gemini-2.5-pro-preview-03-25Sample budget=322025.04 | 37.7 | — | — | 5 | 13.33 | — | — | — | — | — | — | — | — | |
| Thor + Magnushammerenvironment=Isabelle2024.05 | 37.3 | — | — | — | — | — | — | — | — | — | — | — | — | |
| LeanListener2025.03 | 36.9 | — | — | — | — | — | — | — | — | — | — | — | — | |
| GPT-fSample Budget N=64×8×5122025.01 | 36.6 | — | — | — | — | — | — | — | — | — | — | — | — | |
| M2Expert iteration=22022.05 | 35.2 | — | — | — | — | — | — | — | — | — | — | — | — | |
| Thor + expert iterationenvironment=Isabelle2024.05 | 35.2 | — | — | — | — | — | — | — | — | — | — | — | — |