HyperTree Proof Search for Neural Theorem Proving

Benchmark Model Rank Results
automated-theorem-proving-on-metamath-setmmEvariste–Pass@32: 72.4
automated-theorem-proving-on-minif2f-testEvariste–cumulative: 41Pass@64: 41ITP: Lean
automated-theorem-proving-on-minif2f-testEvariste-1d–cumulative: 38.9Pass@64: 38.9ITP: Lean
automated-theorem-proving-on-minif2f-testEvariste-7d–cumulative: 40.6Pass@64: 40.6ITP: Lean
automated-theorem-proving-on-minif2f-testGPT-f–cumulative: 36.6Pass@64: 36.6ITP: Metamath
automated-theorem-proving-on-minif2f-validEvariste–Pass@64: 58.6
automated-theorem-proving-on-minif2f-validEvariste-1d–Pass@64: 46.7
automated-theorem-proving-on-minif2f-validEvariste-7d–Pass@64: 47.5
automated-theorem-proving-on-minif2f-validGPT-f–Pass@64: 47.3