AI RESEARCH
FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
arXiv CS.AI
•
ArXi:2603.26996v1 Announce Type: new We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn from qualifying exams and standard textbooks across topics including analysis, algebra, probability, and logic.