IC-1035Reprover achieves 0% accuracy on sorry theorems in advanced mathematics repositories (PFR, Hairy Ball Theorem, Coxeter) while proving basic theorems in other repositories
Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, Anima Anandkumar
The paper measures reprover's ability to prove previously missing (sorry) theorems across 23 Lean repositories spanning diverse mathematical domains. Reprover fails completely on three advanced-mathematics repositories: the Polynomial Freiman-Ruzsa conjecture (0/37), the Hairy Ball Theorem (0/14), and Coxeter groups (0/15). In contrast, it achieves 48.3% on Mathematics in Lean Source, 20.9% on MiniF2F, and 8.2% on SciLean, which contain more elementary material. The paper attributes this to reprover's training on Mathlib4, which covers primarily undergraduate-level mathematics, making it unable to generalise to advanced topics. On the MiniF2F Lean4 test set, reprover achieves a pass@1 of 34.0% (83/244 theorems).
Evidence
correlational
Key metric
Reprover accuracy: 0% on PFR (0/37), 0% on Hairy Ball (0/14), 0% on Coxeter (0/15); 48.3% on MIL (14/29), 20.9% on MiniF2F (85/406), 8.2% on SciLean (24/294); pass@1 34.0% (83/244) on MiniF2F Lean4 test set
Caveat
The paper notes that some proofs in the PFR repository exploited unintended constructs (placeholder 0=1 statements), and that reprover's performance is limited by Mathlib4's coverage of primarily undergraduate mathematics. The comparison is confounded by the fact that reprover's retriever is also the starting point for LeanAgent.