LEGO-Prover: Neural Theorem Proving with Growing Libraries

Open paper
Benchmark Model Rank Results
automated-theorem-proving-on-minif2f-testLEGO-Prover ChatGPT#6cumulative: 47.1Pass@100: 47.1ITP: Isabelle
automated-theorem-proving-on-minif2f-validLEGO-Prover ChatGPT#4Pass@100: 57.0

Rank counts only results with a code link.