Our new X account is live! Follow @wizwand_team for updates

Formal Theorem Proving on MiniF2F (test)

80.74Pass@1

Kimina-Prover-Preview

Updated 4d ago

Evaluation Results

Method
Kimina-Prover-Preview 2025.04	80.74	-	-	-	-	-	-	-
Kimina-Prover-Preview 2025.04	80.74	-	-	40	86.67	-	-	-
Kimina-Prover-Preview 2025.04	77.87	-	-	-	-	-	-	-
BFS-Prover 2025.04	70.8	-	-	-	-	-	-	-
Kimina-Prover-Preview-Distill-7B 2025.04	70.8	-	-	-	-	-	-	-
Kimina-Prover-Preview 2025.04	68.85	-	-	-	-	-	-	-
Kimina-Prover-Preview 2025.04	68.85	-	-	20	46.67	-	-	-
HunyuanProver v16+BFS+DC 2025.04	68.4	-	-	-	-	-	-	-
CoR-Math-7B 2025.01	66	-	-	-	-	-	-	-
InternLM2.5-StepProver-BF+CG 2025.01	65.9	-	-	-	-	-	-	-
InternLM2.5-StepProver-BF+CG 2025.04	65.9	-	-	-	-	-	-	-
Kimina-Prover-Preview 2025.04	65.16	-	-	-	-	-	-	-
Goedel-Prover-SFT 2025.04	64.7	-	-	-	-	-	-	-
DeepSeek-Prover-V1.5-RL + RMaxTS 2025.01	63.5	-	-	-	-	-	-	-
DeepSeek-Prover-V1.5-RL + RMaxTS 2025.04	63.5	-	-	-	-	-	-	-
Kimina-Prover-Preview-Distill-7B 2025.04	63.1	-	-	-	-	-	-	-
Kimina-Prover-Preview-Distill-1.5B 2025.04	61.9	-	-	-	-	-	-	-
Leanabell-Prover 2025.04	61.1	-	-	-	-	-	-	-
DeepSeek-Prover-V1.5-SFT + RMaxTS 2025.01	60.2	-	-	-	-	-	-	-
DeepSeek-Prover-V1.5-RL 2025.04	60.2	-	-	-	-	-	-	-
DeepSeek-Prover-V1.5-RL + RMaxTS 2025.01	59.6	-	-	-	-	-	-	-
InternLM2.5-StepProver-BF 2025.01	59.4	-	-	-	-	-	-	-
DeepSeek-Prover-V1.5-SFT + RMaxTS 2025.01	56.3	-	-	-	-	-	-	-
Kimina-Prover-Preview-Distill-1.5B 2025.04	56.2	-	-	-	-	-	-	-
SubgoalXL 2024.08	56.1	-	-	-	-	-	-	-
InternLM2.5-StepProver 2025.01	54.5	-	-	-	-	-	-	-
Kimina-Prover-Preview 2025.04	52.94	-	-	-	-	-	-	-
Kimina-Prover-Preview-Distill-7B 2025.04	52.5	-	-	-	-	-	-	-
Lyra 2024.08	51.2	-	-	-	-	-	-	-
InternLM2.5-StepProver-BF+CG 2025.01	50.7	-	-	-	-	-	-	-
LEGO-Prover 2024.08	50	-	-	-	-	-	-	-
InternLM2.5-StepProver-BF 2025.01	47.3	-	-	-	-	-	-	-
Lean-STaR 2025.01	46.3	-	-	-	-	-	-	-
Subgoal-Prover 2024.08	45.5	-	-	-	-	-	-	-
Kimina-Prover-Preview-Distill-1.5B 2025.04	42.6	-	-	-	-	-	-	-
DeepSeek-Prover-V1.5-Base 2025.01	42.2	-	-	-	-	-	-	-
POETRY 2024.05	42.2	-	-	-	-	-	-	-
Hypertree Proof Search 2025.01	41	-	-	-	-	-	-	-
DSP 2024.08	39.3	-	-	-	-	-	-	-
ReProver* 2025.03	37.7	-	-	-	-	-	-	-
gemini-2.5-pro-preview-03-25 2025.04	37.7	-	-	5	13.33	-	-	-
Thor + Magnushammer 2024.05	37.3	-	-	-	-	-	-	-
LeanListener 2025.03	36.9	-	-	-	-	-	-	-
GPT-f 2025.01	36.6	-	-	-	-	-	-	-
M2 2022.05	35.2	-	-	-	-	-	-	-
Thor + expert iteration 2024.05	35.2	-	-	-	-	-	-	-
Thor + expert iteration 2024.08	35.2	-	-	-	-	-	-	-
M1 2022.05	34	-	-	-	-	-	-	-
Hierarchical Attention 2025.04	31.56	-	-	-	-	1.6	0.76	8.11
Hierarchical Attention 2025.04	31.15	-	-	-	-	1.67	0.88	12.5
COPRA (+ Retrieval + Informal) 2023.10	30.74	-	-	-	-	-	-	-
COPRA 2024.05	30.7	-	-	-	-	-	-	-
COPRA (+ Retrieval + Informal) 2023.10	29.92	-	-	-	-	-	-	-
Base model (M0) 2022.05	29.9	-	-	-	-	-	-	-
Thor 2024.05	29.9	-	-	-	-	-	-	-
Thor 2024.08	29.9	-	-	-	-	-	-	-
θ_full (expert iterated on full curriculum) 2022.02	29.6	34.5	-	-	-	-	-	-
FMSCL 2022.05	29.6	-	-	-	-	-	-	-
FMSCL 2024.05	29.6	-	-	-	-	-	-	-
Baseline 2025.04	29.51	-	-	-	-	1.89	-	-
Baseline 2025.04	29.51	-	-	-	-	2.1	-	-
Baseline 2025.04	29.1	-	-	-	-	2.11	-	-
COPRA (+ Retrieval) 2023.10	29.09	-	-	-	-	-	-	-
Hierarchical Attention 2025.04	28.28	-	-	-	-	1.5	0.71	13.24
LLMStep 2025.01	27.9	-	-	-	-	-	-	-
θ_mathlib (expert iterated on mathlib-train) 2022.02	27.2	33	-	-	-	-	-	-
COPRA 2023.10	26.63	-	-	-	-	-	-	-
ReProver 2025.03	26.5	-	-	-	-	-	-	-
Leandojo 2024.05	26.5	-	-	-	-	-	-	-
LLEMMA-7b 2023.10	26.23	-	-	-	-	-	-	-
Baseline 2025.04	26.23	-	-	-	-	2	-	-
Hierarchical Attention 2025.04	26.23	-	-	-	-	1.86	0.93	11.67
θ₁ (value-function based search) 2022.02	25.9	31.1	-	-	-	-	-	-
LLEMMA-34b 2023.10	25.82	-	-	-	-	-	-	-
REPROVER 2023.10	25	-	-	-	-	-	-	-
PACT 2022.02	24.6	29.2	-	-	-	-	-	-
PACT 2022.05	24.6	-	-	-	-	-	-	-
PACT 2024.05	24.6	-	-	-	-	-	-	-
COPRA (- Backtracking) 2023.10	24.59	-	-	-	-	-	-	-
OpenAI o3-mini 2025.04	24.59	-	-	0	6.67	-	-	-
Hierarchical Attention 2025.04	23.36	-	-	-	-	-	-	-
Baseline 2025.04	22.54	-	-	-	-	-	-	-
LLEMMA-7b 2023.10	22.13	-	-	-	-	-	-	-
REPROVER (- Retrieval) 2023.10	22.13	-	-	-	-	-	-	-
LLEMMA-34b 2023.10	21.31	-	-	-	-	-	-	-
Sledgehammer+heuristic 2024.08	20.9	-	-	-	-	-	-	-
Sledgehammer 2023.10	20.49	-	-	-	-	-	-	-
Baseline 2025.04	18.44	-	-	-	-	-	-	-
Code Llama 34b 2023.10	18.03	-	-	-	-	-	-	-
Code Llama 7b 2023.10	17.62	-	-	-	-	-	-	-
Hierarchical Attention 2025.04	17.62	-	-	-	-	-	-	-
Few-Shot (T = 0.7) 2023.10	15.98	-	-	-	-	-	-	-
Baseline 2025.04	14.75	-	-	-	-	-	-	-
Hierarchical Attention 2025.04	14.34	-	-	-	-	-	-	-
Few-Shot 2023.10	13.52	-	-	-	-	-	-	-
Sledgehammer 2024.08	10.4	-	-	-	-	-	-	-
COPRA (GPT-3.5) 2023.10	9.02	-	-	-	-	-	-	-
COPRA (CodeLlama) 2023.10	5.73	-	-	-	-	-	-	-
Few-Shot (GPT 3.5) 2023.10	2.8	-	-	-	-	-	-	-
Few-Shot (CodeLlama) 2023.10	0	-	-	-	-	-	-	-

Showing 100 of 169 rows