| automated-theorem-proving-on-metamath-setmm | Evariste | – | Pass@32: 72.4 |
| automated-theorem-proving-on-minif2f-test | Evariste | – | cumulative: 41Pass@64: 41ITP: Lean |
| automated-theorem-proving-on-minif2f-test | Evariste-1d | – | cumulative: 38.9Pass@64: 38.9ITP: Lean |
| automated-theorem-proving-on-minif2f-test | Evariste-7d | – | cumulative: 40.6Pass@64: 40.6ITP: Lean |
| automated-theorem-proving-on-minif2f-test | GPT-f | – | cumulative: 36.6Pass@64: 36.6ITP: Metamath |
| automated-theorem-proving-on-minif2f-valid | Evariste | – | Pass@64: 58.6 |
| automated-theorem-proving-on-minif2f-valid | Evariste-1d | – | Pass@64: 46.7 |
| automated-theorem-proving-on-minif2f-valid | Evariste-7d | – | Pass@64: 47.5 |
| automated-theorem-proving-on-minif2f-valid | GPT-f | – | Pass@64: 47.3 |