MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

Benchmark Model Rank Results
automated-theorem-proving-on-minif2f-testLean GPT-f#11cumulative: 29.2Pass@1: 24.6Pass@32: 29.2ITP: Lean
automated-theorem-proving-on-minif2f-testLean tidy#18cumulative: 18Pass@1: 18ITP: Lean
automated-theorem-proving-on-minif2f-testMetamath GPT-f#20cumulative: 1.6Pass@1: 1.3ITP: Metamath
automated-theorem-proving-on-minif2f-validMetamath GPT-f#1Pass@8: 2Pass@1: 1
automated-theorem-proving-on-minif2f-validLean GPT-f#2Pass@8: 29.3Pass@1: 23.9
automated-theorem-proving-on-minif2f-validLean tidy#3Pass@1: 16.8