# The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs

arXiv: https://arxiv.org/abs/2506.21621 · HTML: https://mlsanity.com/paper/2506.21621/

## Key facts

- Cited by 30 papers in the map (data through 14 Oct 2026).
- Builds on 40 of its 52 references that are in the map.
- First posted on arXiv 23 Jun 2025.

## Builds on (most cited first, 30 of 40)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [HybridFlow: A Flexible and Efficient RLHF Framework](https://mlsanity.com/paper/2409.19256/) (2024)
- [A Survey on LLM-as-a-Judge](https://mlsanity.com/paper/2411.15594/) (2024)
- [OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems](https://mlsanity.com/paper/2402.14008/) (2024)
- [Large Language Models Cannot Self-Correct Reasoning Yet](https://mlsanity.com/paper/2310.01798/) (2023)
- [LLM Evaluators Recognize and Favor Their Own Generations](https://mlsanity.com/paper/2404.13076/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [rStar-Math: Small LLMs Can Master Math Reasoning with Self-Evolved Deep Thinking](https://mlsanity.com/paper/2501.04519/) (2025)
- [Large Language Models are Better Reasoners with Self-Verification](https://mlsanity.com/paper/2212.09561/) (2022)
- [The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity](https://mlsanity.com/paper/2506.06941/) (2025)
- [MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://mlsanity.com/paper/2505.23281/) (2025)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://mlsanity.com/paper/2410.07985/) (2024)
- [DeepMath-103K: A Large-Scale, Challenging, Decontaminated, and Verifiable Mathematical Dataset for Advancing Reasoning](https://mlsanity.com/paper/2504.11456/) (2025)
- [Mathematical Capabilities of ChatGPT](https://mlsanity.com/paper/2301.13867/) (2023)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategies](https://mlsanity.com/paper/2308.03188/) (2023)
- [A Careful Examination of Large Language Model Performance on Grade School Arithmetic](https://mlsanity.com/paper/2405.00332/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [AIMO-2 Winning Solution: Building State-of-the-Art Mathematical Reasoning Models with OpenMathReasoning dataset](https://mlsanity.com/paper/2504.16891/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Big-Math: A Large-Scale, High-Quality Math Dataset for Reinforcement Learning in Language Models](https://mlsanity.com/paper/2502.17387/) (2025)
- [Beyond Accuracy: Evaluating the Reasoning Behavior of Large Language Models -- A Survey](https://mlsanity.com/paper/2404.01869/) (2024)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [Evaluating Mathematical Reasoning Beyond Accuracy](https://mlsanity.com/paper/2404.05692/) (2024)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)

## Built on by (most cited first, 30 of 30)

- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning](https://mlsanity.com/paper/2511.22570/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs](https://mlsanity.com/paper/2510.04721/) (2025)
- [Reliable Fine-Grained Evaluation of Natural Language Math Proofs](https://mlsanity.com/paper/2510.13888/) (2025)
- [IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation](https://mlsanity.com/paper/2509.26076/) (2025)
- [Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection](https://mlsanity.com/paper/2511.13027/) (2025)
- [Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving](https://mlsanity.com/paper/2507.06804/) (2025)
- [RefGrader: Automated Grading of Mathematical Competition Proofs using Agentic Workflows](https://mlsanity.com/paper/2510.09021/) (2025)
- [The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning](https://mlsanity.com/paper/2603.15914/) (2026)
- [Pessimistic Verification for Open Ended Math Questions](https://mlsanity.com/paper/2511.21522/) (2025)
- [QED-Nano: Teaching a Tiny Model to Prove Hard Theorems](https://mlsanity.com/paper/2604.04898/) (2026)
- [Bolzano: Case Studies in LLM-Assisted Mathematical Research](https://mlsanity.com/paper/2604.16989/) (2026)
- [Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness](https://mlsanity.com/paper/2605.10379/) (2026)
- [TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability](https://mlsanity.com/paper/2608.09538/) (2026)
- [The Mathematician's Assistant: Integrating AI into Research Practice](https://mlsanity.com/paper/2508.20236/) (2025)
- [Putnam-like dataset summary: LLMs as mathematical competition contestants](https://mlsanity.com/paper/2509.24827/) (2025)
- [Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization](https://mlsanity.com/paper/2607.11307/) (2026)
- [ProofVerifier: A Scalable, Diversity-Driven Framework for Natural-Language Proof Verification](https://mlsanity.com/paper/2602.02377/) (2026)
- [STAR-P'olyaMath: Multi-Agent Reasoning under Persistent Meta-Strategic Supervision](https://mlsanity.com/paper/2605.19338/) (2026)
- [Human vs Machine Mathematical Difficulty on Project Euler: An Experimental Analysis](https://mlsanity.com/paper/2606.21972/) (2026)
- [Cost-Effective Automated Judging of Natural-Language Mathematical Proofs](https://mlsanity.com/paper/2608.00004/) (2026)
- [Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning](https://mlsanity.com/paper/2602.00998/) (2026)
- [Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints](https://mlsanity.com/paper/2604.15713/) (2026)
- [AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification](https://mlsanity.com/paper/2607.11849/) (2026)
- [Reasoning Errors Have a Region and a Direction in the Residual-Stream Trajectory of LLMs](https://mlsanity.com/paper/2608.05660/) (2026)
- [PCFBench: A Diagnostic Benchmark for Product Carbon Footprint Estimation](https://mlsanity.com/paper/2608.27716/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Splicing Hints into Reasoning Traces: Learning from Demonstrator Failures](https://mlsanity.com/paper/2610.13996/) (2026)
- [One-Sided Verification Under Limited Expert Review](https://mlsanity.com/paper/2610.18089/) (2026)

## Abstract (arXiv)

In recent months, large language models (LLMs) have made significant progress in mathematical proof generation, but further advancement is hindered by the lack of a large-scale, high-quality dataset of human-evaluated proofs. While expensive to create, such a dataset is essential for driving improvements in training and enabling a rigorous analysis of proof generation capabilities. In this work, we present the Open Proof Corpus (OPC), a dataset comprising over 5,000 human-evaluated proofs produced by state-of-the-art LLMs. The OPC was specifically designed for broad applicability and downstream usage in proof generation research and is the first to include a substantial number of correct, LLM-generated solutions to problems from prestigious mathematics competitions such as the USAMO and IMO. Using the OPC, we explore critical questions in automated proof generation: (1) the performance gap between natural language and formal proof generation, (2) the discrepancy between final-answer accuracy and full-proof validity, and (3) the impact of best-of-n selection on proof quality. Finally, to showcase the utility of the OPC, we finetune an 8B-parameter model on the dataset, obtaining a model that performs on par with the best model, Gemini-2.5-Pro, on the task of evaluating proof correctness.