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

Understand

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.