The Open Proof Corpus

The Open Proof Corpus is the largest public dataset of human-graded LLM-generated mathematical proofs — over 5,000 proofs with expert human evaluations — built to study how well models produce rigorous, correct proofs (not just final answers) and to train/benchmark automated proof graders. From Vechev's SRI Lab (joint→INSAIT; ETH SRI leads), a companion to the MathArena effort.