Automated Theorem Proving on miniF2F-test

Metric: cumulative (higher is better)

LeaderboardDataset

Loading chart...

Results

Hide extra data

#	Model↕	cumulative▼	Extra Data	Paper	Date↕	Code
1	Kimina-Prover-Preview	80.74	Yes	Kimina-Prover Preview: Towards Large Formal Reas...	2025-04-15	Code
2	ProofAug	66	No	Efficient Neural Theorem Proving via Fine-graine...	2025-01-30	Code
3	DeepSeek-Prover-V1.5	63.5	Yes	DeepSeek-Prover-V1.5: Harnessing Proof Assistant...	2024-08-15	Code
4	Subgoal-XL	56.1	Yes	SubgoalXL: Subgoal-based Expert Learning for The...	2024-08-20	Code
5	DeepSeek-Prover	52	Yes	DeepSeek-Prover: Advancing Theorem Proving in LL...	2024-05-23	-
6	Lyra + GPT-4	47.1	No	Lyra: Orchestrating Dual Correction in Automated...	2023-09-27	Code
7	LEGO-Prover ChatGPT	47.1	No	LEGO-Prover: Neural Theorem Proving with Growing...	2023-10-01	Code
8	Decomposing the Enigma	45.5	No	Decomposing the Enigma: Subgoal-based Demonstrat...	2023-05-25	Code
9	Evariste	41	Yes	HyperTree Proof Search for Neural Theorem Proving	2022-05-23	-
10	Evariste-7d	40.6	No	HyperTree Proof Search for Neural Theorem Proving	2022-05-23	-
11	Evariste-1d	38.9	No	HyperTree Proof Search for Neural Theorem Proving	2022-05-23	-
12	DSP (540B Minerva informal)	38.9	No	Draft, Sketch, and Prove: Guiding Formal Theorem...	2022-10-21	Code
13	Lean Expert Iteration	36.6	Yes	Formal Mathematics Statement Curriculum Learning	2022-02-03	Code
14	GPT-f	36.6	No	HyperTree Proof Search for Neural Theorem Proving	2022-05-23	-
15	Thor + expert iteration on autoformalised theorems	35.2	Yes	-	-	-
16	COPRA + GPT-4-turbo	30.7	No	An In-Context Learning Agent for Formal Theorem-...	2023-10-06	Code
17	Thor	29.9	No	Thor: Wielding Hammers to Integrate Language Mod...	2022-05-22	-
18	Lean GPT-f	29.2	No	MiniF2F: a cross-system benchmark for formal Oly...	2021-08-31	Code
19	MMOS-DeepSeekMath-7B	28.3	No	An Empirical Study of Data Ability Boundary in L...	2024-02-23	Code
20	ReProver	26.5	No	-	-	-
21	LLEMMA-7b	26.2	No	Llemma: An Open Language Model For Mathematics	2023-10-16	Code
22	LLEMMA-34b	25.8	No	Llemma: An Open Language Model For Mathematics	2023-10-16	Code
23	PACT (reproduced by Thor)	24.6	No	Proof Artifact Co-training for Theorem Proving w...	2021-02-11	Code
24	COPRA + GPT-4	23.3	No	An In-Context Learning Agent for Formal Theorem-...	2023-10-06	Code
25	Sledgehammer + heuristics	20.9	No	Draft, Sketch, and Prove: Guiding Formal Theorem...	2022-10-21	Code
26	Lean tidy	18	No	MiniF2F: a cross-system benchmark for formal Oly...	2021-08-31	Code
27	COPRA + GPT-3.5	11.9	No	An In-Context Learning Agent for Formal Theorem-...	2023-10-06	Code
28	Sledgehammer	10.4	No	Thor: Wielding Hammers to Integrate Language Mod...	2022-05-22	-
29	Metamath GPT-f	1.6	No	MiniF2F: a cross-system benchmark for formal Oly...	2021-08-31	Code