Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

Benchmark Model Rank Results
automated-theorem-proving-on-minif2f-testDSP (540B Minerva informal)#8cumulative: 38.9Pass@100: 38.9ITP: Isabelle
automated-theorem-proving-on-minif2f-testSledgehammer + heuristics#17cumulative: 20.9Pass@1: 20.9ITP: Isabelle
automated-theorem-proving-on-minif2f-validDSP (62B Minerva informal)#6Pass@100: 43.9