{"id":"arxiv:2603.26996","kind":"preprint","title":"FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?","authors":["Nikil Ravi","Kexing Ying","Vasilii Nesterov","Rayan Krishnan","Elif Uskuplu","Bingyu Xia","Janitha Aswedige","Langston Nashold"],"author_count":8,"year":2026,"published":"2026-03-27","venue":null,"cited_by":null,"doi":null,"arxiv_id":"2603.26996","nct_id":null,"source_url":"https://arxiv.org/abs/2603.26996","archive_url":"https://space-kitty.com/papers/arxiv:2603.26996","updated":"2026-03-27","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/2603.26996","abstract":"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. We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy, with performance dropping rapidly after that. In addition to the accuracy numbers, we also provide empirical analysis of tool-use, failure modes, cost and latency, thereby providing a thorough evaluation of the formal-theorem proving abilities of frontier models.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.AI","cs.CL","cs.LG","cs.PL"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[],"cited_in_dossiers":[]}