TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

Alexander K Taylor, Junyi Zhang, Ethan Ji +10

Automated theorem proving (ATP) benchmarks largely consist of problems formalized in MathLib, so current ATP training and evaluation are heavily biased toward MathLib's definitiona…