FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914429063397376 |
|---|---|
| author | Ravi, Nikil Ying, Kexing Nesterov, Vasilii Krishnan, Rayan Uskuplu, Elif Xia, Bingyu Aswedige, Janitha Nashold, Langston |
| author_facet | Ravi, Nikil Ying, Kexing Nesterov, Vasilii Krishnan, Rayan Uskuplu, Elif Xia, Bingyu Aswedige, Janitha Nashold, Langston |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_26996 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified? Ravi, Nikil Ying, Kexing Nesterov, Vasilii Krishnan, Rayan Uskuplu, Elif Xia, Bingyu Aswedige, Janitha Nashold, Langston Artificial Intelligence Computation and Language Machine Learning Programming Languages 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. |
| title | FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified? |
| topic | Artificial Intelligence Computation and Language Machine Learning Programming Languages |
| url | https://arxiv.org/abs/2603.26996 |