Automated Theorem Proving on miniF2F-test

Metric: Pass@1 (higher is better)

LeaderboardDataset

Loading chart...

Results

Submit a result

Hide extra data

#	Model↕	Pass@1▼	Extra Data	Paper	Date↕	Code
1	Kimina-Prover-Preview	52.94	Yes	Kimina-Prover Preview: Towards Large Formal Reas...	2025-04-15	Code
2	ProofAug	36.5	No	Efficient Neural Theorem Proving via Fine-graine...	2025-01-30	Code
3	Thor + expert iteration on autoformalised theorems	35.2	Yes	-	-	-
4	COPRA + GPT-4-turbo	30.7	No	An In-Context Learning Agent for Formal Theorem-...	2023-10-06	Code
5	DeepSeek-Prover	30	Yes	DeepSeek-Prover: Advancing Theorem Proving in LL...	2024-05-23	-
6	Thor	29.9	No	Thor: Wielding Hammers to Integrate Language Mod...	2022-05-22	-
7	Lean Expert Iteration	29.6	Yes	Formal Mathematics Statement Curriculum Learning	2022-02-03	Code
8	MMOS-DeepSeekMath-7B	28.3	No	An Empirical Study of Data Ability Boundary in L...	2024-02-23	Code
9	Lean GPT-f	24.6	No	MiniF2F: a cross-system benchmark for formal Oly...	2021-08-31	Code
10	PACT (reproduced by Thor)	24.6	No	Proof Artifact Co-training for Theorem Proving w...	2021-02-11	Code
11	COPRA + GPT-4	23.3	No	An In-Context Learning Agent for Formal Theorem-...	2023-10-06	Code
12	Sledgehammer + heuristics	20.9	No	Draft, Sketch, and Prove: Guiding Formal Theorem...	2022-10-21	Code
13	Lean tidy	18	No	MiniF2F: a cross-system benchmark for formal Oly...	2021-08-31	Code
14	COPRA + GPT-3.5	11.9	No	An In-Context Learning Agent for Formal Theorem-...	2023-10-06	Code
15	Sledgehammer	10.4	No	Thor: Wielding Hammers to Integrate Language Mod...	2022-05-22	-
16	Metamath GPT-f	1.3	No	MiniF2F: a cross-system benchmark for formal Oly...	2021-08-31	Code