The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs
Authors: Jasper Dekoninck
Ivo Petrov
Kristian Minchev
Miroslav Marinov
Maria Drencheva
Lyuba Konova
Milen Milenov Shumanov
Kaloyan Tsvetkov
Nikolay Drenchev
Lazar D. Todorov
Kalina Nikolova
Nikolay Georgiev
Vanesa Kalinkova
Margulan Ismoldayev
Mislav Balunovic
Martin Vechev
Venue: ICLR 2026 Poster (2026)
Keywords: ai
artificial intelligence
reasoning
llm
math
benchmark
dataset
proof
gpt
machine learning
Primary area: datasets and benchmarks
TL;DR: We conduct the largest human-based evaluation of frontier Large Reasoning Models on challenging mathematical proofs and answer multiple open questions in the field.

Abstract: 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 addressing key open questions in the field of automated proof generation. Specifically, it remains unknown (1) how large the gap is between natural language and formal proof generation, (2) how final-answer accuracy relates to full proof correctness, and (3) how best-of-n selection strategies can affect proof quality. 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 large dataset of LLM-generated solutions to problems from prestigious mathematics competitions such as the USAMO and IMO. Using the OPC, we address the open questions outlined above and provide new insights into LLMs' strengths and limitations in mathematical reasoning. Finally, to showcase the utility of the OPC, we finetune an 8B-parameter model on the dataset, obtaining a model that matches Gemini-2.5-Pro, and performs close to the best model, GPT-5, on evaluating proof correctness.

Published as a conference paper at ICLR 2026
THE OPEN PROOF CORPUS: A LARGE-SCALE STUDY OF LLM-GENERATED MATHEMATICAL PROOFS
Jasper Dekoninck Ivo Petrov Kristian Minchev?, Mislav Balunović Martin Vechey
ETH Zurich PINSAIT, Sofia University "St. Kliment Ohridski" jasper dereer.dekonnckkinn.. sttpne.ch..o..perroeeeee www.peetooeeimsiit.aa
Dataset Contributors: Miroslav Marinov', Maria Drencheva', Lyuba Konova*
Milen Shumanov2 Kaloyan Tsvetkov2, Nikolay Drenchev?, Lazar Todorov²
Kalina Nikolova Nikolay Georgiev?, Vanesa Kalinkova², Margulan Ismoldayev25
IInttitte of Mathematics and Informatics, Bulgarian Academy of Sciences
Sooia University "St. Kliment Ohridski" >aasaccuseetts Institute Technology
https://proofcoopus.aaj
attps://luugingfaccccoo/ttttttts http::///
ABSTRACT
In recent months, large language models (LLMs) have made significant progress in mathematical proof generation, but further advancement is hindered by the lack of large-scale, high-quality dataset of human-evaluatee proofs. While expen- sive to create, such a dataset essential for driving improvements in training and addressing key open questions in the field of automated proof generation. Specif- ically, remains unknown (1) how large the gap between natural language and formal proof generation, (2) how final-answer accuracy relates to full proof cor- rectness, and (3) how best-of-n selection strategies can affect proof quality. In this work, we present the Open Proof Corpus (OPC), dataset comprising over 5,000 human-evaluated proofs produced by state-of-the-arr L.MMs. The OPC was specif- ically designed for broad applicability and downstream usage in proof generation research and is the first large dataset of LLM--ennrated solutions to problems from prestigious mathematics competitions such the USAMO and IMO. Using the OPC, we address the open questions outlined above and provide new insights into LLMs' strengths and limitations in mathematical reasoning. Finally, showcase the utility of the OPC, we finetune an 8B 18-parameter model on the dataset, obtain- ing model that matches GEMINI-2.5 2.5-N--2.PPPGG. PRO, and performs close the best model, GPT-5, on evaluating proof correctness.
INTRODUCTION
Large language models (LLMs) have recently achieved impressive progress in mathematical reason- ing, obtaining top-competitor performance on various final-answer benchmarks such as AIME and HMMT (Balunović al. 2025). However, growing evidence suggests that these benchmarks fail to capture the full range of mathematical capabilities, as they do not require models to produce proofs detailed intermediate steps (Mahdavi et al.) 2025 Guo et al. (025b). Such step-by-step reasoning critical for applications in theorem proving, mathematical research, and education.
Proof benchmarking To address this, several evaluation efforts have taken place, revealing that LLMs significantly underperform proof generation compared existing final-answer bench- marks (Petrov et al., 2025) Mahdavi et al. 2025). Despite their value, these benchmarks are severely limited their use for broader analysis and training. Specifically, they are small (Petrov al. 2025
Guo et al.) 2025b). use outdated models (Frieder et al. 2023), contain few correct proofs (Mahdavi
al. 2025 and are not open-sourced (Mahdavi et al.
2025 Guo al. 2025b).
"Equal contribution.

---

Published as a conference paper at ICLR 2026
Sample
50%
Problem: EGMO 2012, Problem
75%
Level: High School
5.%
40%
Split: Generic
25%
20%
Question: Solve over functional equation fluf(a f())) 4 2y
Human
Best Medul
Formal
vnfomml
Coreec Anverr
35%
Proof:
To solve the functional equation we that **nly** solution.
45%
50%
Grade (Incorrect); The model substitutes be 1. All further ideas are based on the wrong assumption.
35%
23%
Rasagn
25%
03
Gemmn-Pr
5
(a) Sample from the OPC
(b) Conclusions from the OPC
Figure 1: Overview of the OPC and its conclusions. On the left, we show a typical sample, including question from a high-quality mathematical competition, LLM-ggnerated proof, and a human judgment of proof correctness. On the right, we summarize the main conclusions from the OPC.
Open questions Furthermore, key questions about proof generation capabilities remain unan- swered. First, while is widely claimed that there is a gap between final-answer performance and proof generation capabilities, this claim has not yet been supported by evaluating LLM- generateed proofs on existing final-answer benchmarks. Second, despite recent advances in formal proof gener- ation with Lean (Chen et al.) 2025 Lin al. (0255), the performance gap between natural language and formal proof generation remains unclear. Third, the potential of best-of-n selection strategies to improve proof quality has been explored.
To address these challenges, we introduce the Open Proof Corpus (OPC): large-scale, human-validated dataset comprising over 5,000 LLMM-genrated proofs across more than 1,000 problems. As shown in Fig. [(a)] each OPC sample includes (1) a problem from high-quality mathematical competition such as the International Mathematical Olympiad, (2) a proof generated by a state-of-the-art LLM, and (3) binary human evaluation of the proof's correctness with feedback. The OPC was specifically designed for downstream usage in proof gener- ation research, enabling both training and evaluation of LLMs on proof generation tasks. To address the open questions outlined earlier, the OPC includes problems from specific sources: problems from the PutnamBench (Tsoukalas et al.) 2024) enable comparisons between formal and informal reasoning, while problems from MathArena (Balunović et al. 2025) support evaluation of proof correctness for problems with final answers.
Our work: the Open Proof Corpus
Key findings Despite the difficulty of problems in the OPC, state-of-the-art LLMs demonstrate surprisingly strong performance. For instance, 04-MINT correctly solves almost 20% of the prob- lems the IMO Shortlist, and the OPC generally consists of 43% correct proofs. Furthermore, as
shown in the top left of Fig. [(b)] LLMs exhibit strong capabilities in evaluating proof's: GPT-5 achieves 90.8% accuracy in judging proof correctness, which is on-par with human performance on this task. To showcase the utility of the OPC, fine-tune R 21-QWEN3-8B (Guo et al. 2025a) using
GRPO (Shao et al., 2024) on the OPC, resulting in an open model that achieves 88. 08.1% judgment accuracy, close to top models like GPT-5 and outperforming the majority of frontier models.
Answering open questions The OPC allows us to empirically resolve the open questions outlined above, with all conclusions shown in Fig. [[b] First, as shown on the top right, find that natu- ral language proof generation significantly outperforms formal proof generation: on PutnamBench, GEMINI-2.5-PAR solves 4 times more problems than the best formal model, GOEDEL--ROVER. V2 (Lin et al. 2025b). Second, as shown on the bottom left, we observe a substantial gap between final-answer accuracy and proof correctness. While CEMINI-2.5-PHR loses only 8% of its final- answer accuracy when proof correctness is required, 03 suffers a drop of almost 30%. Third, as shown on the bottom right, we find that best-of-n strategies yield large gains performance. In- terestingly, while standard best-of-n selection methods moderately improve accuracy from 26% to 36%, ranking approach inspired by (Liu et 2025) achieves the highest performance of 47%.
2

---

Published as a conference paper at ICLR 2026
Main Contributioos
Our key contributions are:
A rigorous pipeline for generating and evaluating natural language proofs (
The OPC, human-validated dataset comprising over 5,000 -ggeerrrertted proofs ($4)
Resolution of open questions in natural language proof generation using the OPC ($5).
An open-source, 8B-parameter model fine-tuned on the OPC that achieves 88. 1..1% % judgment accuracy, close the best model on this task ($5).
RELATED WORK
We briefly discuss the relevant literature on mathematical reasoning benchmarks and datasets.
Final-answer benchmarks Final-answer benchmarks evaluate models by comparing a final an- swer from the model's 's output with a ground-truth answer, typically using rule-based parsers. With the rise of reasoning LLMs (Jaech et al. (2024), older benchmarks have become saturated (Cobbe
al., 202T]] Lightman al. 2024). and more recent ones are nearing saturation (Gao et al. [025
He et al. 2024, Balunović et al. 2025). Only private benchmarks such as FrontierMath (Glazer al. 2024) remain sufficiently challenging for the latest models. However, this benchmark does
not require the generation of full proofs or detailed reasoning steps. Moreover, its private nature
hinders reproducibility and broader community engagement, both key factors in driving progress.
Formal proof generation Another growing line of work involves training LLMs to generate for- mal proofs in languages such as Lean (de Moura and Ullrich| (22T)) or Isabelle (Nipkow et al.)
2002). which can then be automatically verified by these systems (Zheng et al. 2022 Tsoukalas et al. 2024 Yu et al. 2025). While this paradigm enables rigorous correctness checking, it typically requires models to be specifically finetuned for formal proof generation (Ren et al.. 2025 Wang
et al. 2025 Lin et al. 2025a). In contrast, state-of-the-ar general-purpose models like GPT-5 and struggle with formal proof generation. As result, formal reasoning currently
GEMINI-2.5-PPP
does not make full use of the natural language capabilities of these general-purge purpose models, and, as
we show in $5 there remains a significant performance gap between formal and natural language proof generation, with the latter being substantially more effective.
Proof-generation evaluation efforts Going beyond final- anal-a accuracy has gained recent at- tention, with several works investigating the reasoning traces of recent LLMs to identify patterns and potential for improvement (Shojace al. 2025] Mondorf and Plank 2024 Xia et al. 2025). How-
ever, only few studies have focused directly on evaluating full proots. Petrov et al. (2025) evaluated LLMs on the six problems from the USAMO 2025, uncovering significant flaws in the generated proof'. Similarly, Mahdavi et al. (2025) evaluated LLM performance on a large set of IMO Shortlist problems, finding that no model surpassed 5% accuracy. In contrast, Frieder et al. (2033 reported
that GPT-3.5 and GPT-4 performed well on simpler tasks, generating correct proofs in significant fraction of cases. Still, all these studies are limited by either the use of outdated models or the small scale of their evaluations.
Two recent works have expanded this line of research. Sheng et al. (2025) focus specifically on inequality proofs and primarily emphasize the development of L.M judge framework to mitigate the high cost of human evaluation. Guo et al. (2025b) highlight notable gap between final- answer accuracy and the ability to generate correct proofs, a finding we confirm in $5 However, their analysis stops at this observation and does not evaluate performance on an established final- answer benchmark. Further, both studies are limited in scale compared to the OPC and have not open-sourced their muman-annotated proofs.
Automated proof grading with LLMs as judges The growing capabilities of LLMs have led to the "LL-M-as-a- judge" paradigm, which enables cost-effective evaluation of complex model outputs (Zheng et al. 2023 Gu et al. 2024 Chevalier et al. 2024).. Recent work has extended this approach to mathematical proof evaluation (Sheng et al. 2025| Zhao et al. 2024 2025). These studies report promising results, showing that LLMs can grade specific types of problems with reasonable relia-
bility (Sheng et al. 2025| Zhao al. (024) and can provide useful feedback in educational settings
(Zhao et al., 2024; 2025). This work builds on these insights, building a dataset of evallaeedl
proof' to further improve LLM judging capabilities, detailed in
3

---

Published as a conference paper at ICLR 2026
Mathematical training datasets Several large-scale datasets have been developed train LLMs
on mathematical reasoning. One of the earliest, Li et al. (2024), compiled a large dataset of internet- sourced problems, including both final-answer questions and natural language proofs. However, it
lacks L..M-genertted proofs, human judgments, and examples of incorrect proofs. Other datasets
have focused exclusively final-answer tasks (Albalak et al.) [2055] He et al. 2025 Moshkov
et al. 2025), offering limited support for training or evaluating proof generation. Finally, Zhang
al. (2025) introduced a dataset of both valid and invalid problem statements, each accompanied
by LLM L-generrtee proofs. While this ensures that incorrect proofs exist for invalid statements, the
dataset does not include human evaluation of proofs or other information on proof validity.
METHODOLOGY
Accurately evaluating LLM-generated proof's is a challenging task. Models often make difficult- to-detect errors, and they rarely acknowledge when they cannot solve a problem (see { In this section, we outline the methodology used to create the OPC, with particular emphasis the com- plexities of evaluating Len-rerrrated proof' and our efforts to maximize dataset size. Since human judges cannot reasonably spend hours studying each problem, efficient grading. This pipeline consisted of three main components: problem and judge prepara- tion () the grading procedure ($3.2). and monitoring and validation ($3.3). The dataset was constructed over a period of four weeks, involving 13 expert judges and generating over 5,000 human-validated proofs.
developed pipeline support
3.1 PROBLEM AND JUDGE PREPARATION
Judge selection Judges were selected from among former IMO participants or individuals who reached the final stages of IMO selection in their countries. We contacted each judge personally to ensure they were qualified and motivated. A total of 13 judges were involved, each responsible for grading a varying number of problems. Three of the most active judges had prior experience with evaluating LLM-generated proofs. One judge served as the coordinator, maintaining regular communication, tracking progress, and ensuring consistency and motivation across the group.
Problem selection Problems were drawn from top-tier national and international mathematics competitions, such as the USAMO and IMO, to capture a balanced mix of correct and incorrect proofs. In particular, we included competitions based on two informal criteria: (1) the competition is well-known and produces high-quality problems, and (2) the difficulty level of the competition aligns with target of roughly 50% model accuracy. All problems were sourced from official materials. Non-English problems were translated using GPT--41 and manually verified for accuracy by the coordinator. When available, official ground-truth solutions were also extracted and provided to the judges as references.
Throughout the annotation process, model performance was actively monitored to ensure that the selected problems remained appropriately challenging. For instance, more problems from interna- tional competitions were added when initial results indicated that models were performing very well (>= 65%) on national-leve problems. Each day, problem prioritization was adjusted based on ongo- ing performance metrics, judge availability, and progress towards the specific conclusions we aimed to draw from the dataset.
Proof generation Proofs were generated using a set of state-of-the-art LLMs known for their strength in mathematical reasoning. Specifically, we used 04-MINI and 03 from OpenAl (Ope-)
nAl 2025). GEMINI-2.5-PRO from Google (Team] 2025), GROK-3-Min from XAI (xAI 2025), QWEN3 1335-A222 from Qwen (Qwen Team| 2025). and the latest version of R from DeepSeek [Guo et al. 2025a). RI was released mid-way through dataset construction and replaced GROK-3- MINI thereafter. We designed the model prompt to clearly instruct models to generate full solutions, refining it through small-scale pilot tests. The final prompt is shown in $1.1 All models were run with default parameters and a maximum generation length of 64,000 tokens. For the MathArena subset (Balunović et al. 2025), we only retained solutions with a correct final answer, retrying gen- eration necessary. For PutnamBench (Tsoukalas et al. 2024), we appended the informal final answer (if present) to the problem statement to mirror the setup for formal models, allowing direct comparison between natural and formal proof outputs.
4

---

Published as a conference paper at ICLR 2026
3.2 GRADING PROCEDURE
User interface We built a custom web interface to facilitate efficient grading. A sample instance is available in our supplementary material, with screenshots included in $ The interface displays the problem, reference solution (if available), anonymized model-generatee Judges could mark the problem or solution as malformed (to filter such cases from the dataset), grade the proof, and annotate sentences from the model-generatee generated proof with comments. Continuous feedback from judges helped us refine the interface over time.
proof, and grading form.
Judge instructions Judges were asked to label proofs as either correct or incorrect and provide written justification. Precise grading guidelines were critical to avoid inconsistencies in edge cases, such as minor omissions or shortcuts. To prevent overly strict grading, we clearly defined what level of omissions and frequency of mistakes were acceptable in correct proof. The full guidelines available in our supplementary material, with summary in { These instructions were developed collaboratively with the judges and finalized after pilot phase (see $3.3).
Abstention and uncertainty Judges were allowed to abstain from grading proof if they lacked the necessary expertise or found the solution too complex or convoluted. They could also mark judgments as uncertain in borderline cases, which proved especially useful for near-correct proofs containing subtle errors. Less than 3% of proof' the OPC are flagged as uncertain.
LLM issue summaries After several hundred graded proofs, we introduced a new feature to sup- port grading: an automatically generated summary of the proof using 04-MINI. These summaries flagged potential issues, such as logical gaps or missing steps, based on a specially designed prompt (see .1.2). Importantly, the model was instructed not give a final verdict. Judges reported that this significantly improved their efficiency and accuracy in detecting errors. To ensure the inclusion of these summaries did not bias our judges, we evaluated the agreement rate between 04-MINI as judge and human graders before and after their introduction. There was no significant difference in agreement, indicating that no bias was introduced into the grading process. However, in experiments involving rest-of-n selection, where the LLM judge acts as a selection mechanism, we omitted these summaries to avoid any form of compounding bias in the evaluation.
Problem distribution Problems were assigned to judges based on background and availability. Judges not qualified to evaluate andergraduate-levar problems were excluded from grading them. To ensure balanced workload, we monitored grading progress and dynamically reassigned problems needed.
3.3 MONITORING AND VALIDATION
To ensure grading quality and judge consistency, we implemented a set of validation procedures.
One experienced judge was assigned as coordinator, responsible for tracking grading progress, resolving issues, and ensuring motivation. As author, the coordinator had detailed knowledge of the dataset's goals and methodology and was available to answer judges' questions.
Coordinator
Developer In addition to the coordinator, one of the core authors served developer, providing technical support for the grading interface and addressing any software-related issues that arose during the grading process. Judges were encouraged to report bugs or suggest improvements to the grading interface, which the developer would address immediately to ensure smooth grading experience. The developer was also responsible for implementing new features, such as the L.MM- generated issue summaries, and to monitor model performance metrics to inform problem selection and judge assignments.
Pilot phase Before full-scale grading, we conducted test with limited number of problems. In particular, four experienced judges graded approximately 300 proofs in this initial stage. Dur- evaluate
ing this phase, more significant portion of proofs (around 35%) were double-graded inter-judge consistency. Judges were also very actively monitored, and encouraged to actively ask questions about any small ambiguity they encountered. After this stage, judge feedback was col- lected to improve the grading interface and instructions. In particular, the instructions were refined address remaining ambiguities and edge cases.
5

---

Published as a conference paper at ICLR 2026
Monitoring discrepancies In total, approximately 10% of the proofs double-gradee to eval- uate jater-judge consistency. Throughout the grading pipeline, disagreements were reviewed by the coordinator to determine whether they arose from misunderstandings ambiguous instructions, or emross overlooked by a judge. If possible, instructions were further improved to prevent similar is- sues. However, most inconsistencies came from overlooked errors in the proofs and could therefore not be resolved by clarifying the instructions. If the coordinator identified a significant number of discrepancies for specific judge, they would discuss the issue with the judge clarify instructions.
OPEN PROOF CORPUS
We now introduce the OPC and provide overview of key dataset statistics. At high level, the OPC built to support training and to facilitate a rigorous analysis of proof generation capabilities.
Basic properties The OPC consists of 5,062 proofs across 1,010 distinct problems, gener- ated by six state-of-the-ard L.MMs. Each proof is labeled either correct incorrect by one or two human judges. Labels are accompanied by short justifications, with optional annota- tions highlighting specific sentences within the proof. Each problem may also include data such as its competition source, difficulty level, and other relevant attributes. An example is shown in Fig. I(a)
Other
IMOSL
16.4%
17.6%
12ho
IMC
12. 12.1%
Putnam
EGMO
4.7%
5.0%
Iiss
7.9%
USAMO
Competitions Problems were sourced from wide range of prestigious mathematics compe- titions. A full breakdown is provided in $Λ
BalticWay
Figure 2: Overview of competitions the OPC.
with summary shown in Fig. A also reports the average accuracy of the best best-performing model per competition, offering a rough proxy for difficulty. Most problems are at the high school level (es 84%), with small portion drawn from undergraduate-llvel competitions ( 16%).
Models Table 1 shows the number of proofs generated
Table Solutions per evaluated model.
by each model. Not all models attempted every problem, but most problems include solutions from five models. 04-MINI contributed the largest number of proofs, as it was used in the best-of-n and pass @ experiments.
Model
# Solutions
04-MINI
1615
03
892
QWEN3-235B-A22B
890
Human performance To estimate label reliability, we coublleggrade approximately 10% of the dataset. Among these, judges agreed on the proof's s correctness in 90.4% of cases. Assuming independent judgments, we can esti-
GEMINI-PRO
878
GROK-3-MINI
461
DEEPSEEK-RI
326
mate the individual judge error rate p by solving 0.904 = (1 p)2 + p2, giving = 5%. This
indicates low noise level, which expected for a human-annotated dataset of this complexity.
Data splits
The OPC is divided into four subsets, each serving a distinct purpose:
MathArena: A subset of 112 problems from MathArena (Balunović et al. 2025 final- answer benchmark for mathematical reasoning.
PutnamBench: A subset of 114 problems from PutnamBench (Tsoukalas al. 2024 used to compare natural language and formal proof generation.
Best-of-n: A subset of 152 problems from hard competitions, each solved multiple times by 04-MINT. For 60 of these problems, all 8 generations were human-evaluated The rest include judgments only for the generations selected by a best-of-n selection strategy.
Generic: A subset of 676 problems from various competitions, solved by multiple models.

---

Published as a conference paper at ICLR 2026
80%
First Partition Second Partition
19.1%
60%
$4.0%
50.0%
75 815
40%
25,2%
Not Applicable
Not Applicable
20%
0%
Gemini
o4-mini
Qwen3
Grok-Mini
X
Figure 3: Average proof correctness on the OPC. Data is split into two partitions, the first, resp. sec- ond, containing only problems answered by all models except R1, resp. partition contains problems from more challenging competitions, explaining the score discrepancy.
The second
The MathArena and PutnamBench subsets are drawn from existing benchmarks and should not be used for training. The generic and best-of-n subsets intended for training, validation, and further analysis. However, small portion of the generic subset is held back for benchmarking purposes.
5 RESULTS
We present main findings. In $5.1 evaluate the proof-generatie capabilities of vari- ous models. $5.2 evaluates the ability of LLMs to judge proof correctness. In $5.3 we compare informal and formal proof-generation performance. $5.4 analyzes proof correctness given correct final answers. $5.3 examines the effectiveness various best-of-n strategies. Finally, in $5.6) we discuss the potential impact of data contamination on our results. In $ we additionally provide some qualitative observations about common mistakes in the generated proofs.
All shown confidence intervals in this section 95% intervals computed using the large sample normal approximation. Bold numbers indicate the best performance in the respective category, and underlined numbers are within the confidence interval of the best performance.
5.1 PROOF GENERATION CAPABILITIES
Proof generation results Fig. shows the average proof correctness of each model on subset of the OPC, including only GEMINI-2.5-PRE achieves the highest accuracy, slightly outperforming 04-MINI. In contrast, the two open-source models, QWEN3-233 2-55-A22BB and R1, underperform significantly, highlighting performance gap between closed- and open-source models generating correct proofs.
questions for all models except GROK-3-MINI or R1.
Uncertainty acknowledgment Out of more than 1,700 incorrect solutions analyzed, models plicitly state their inability to solve the problem in only 114 instances, with all but five of those generated by 03. Even 03 more likely produce an incorrect proof than acknowledge uncer- tainty. This reluctance to admit failure highlights key limitation. In domains like mathematics, this could undermine trust in systems that rely on LLMs for provably correct solutions.
5.2 LLMS ARE HUMAN LEVEL JUDGES
Setup The OPC provides binary human judgments for proof correctness, making ideal for training and evaluating LLM proof judges. To leverage this, we split the generic sub- set by problem into training and test sets. Using GRPO (Shao et al., 2024), we fine-tune R1-QWEN3-8B using human labels for rewards. The test set comprises 293 LLM-ggnerated proofs with 40% average correctness. We evaluate both reasoning models, such as GPT- 5, and general-purpose models like 1PT-4.1. Importantly, the human baseline is not mea-

---

Published as a conference paper at ICLR 2026
82.7%
76.5%
80%
61,555
60%
77.0%
$2.2%
76.7%
55%
20%
25%
0%
Gurrers-YY
p4-mini
Querd
Grok-iri
x
Olenn'
Figure 4: Average proof correctness on the Put- namBench.
Figure 5: Comparison of final-answer accuracy and proof correctness on the MathArena subset.
sured on the test subset, but rather on all double-graded proofs in the OPC. Since the test samples are uniformly drawn from the OPC, this does not significantly affect the comparison.
Table 2: LLMs as proof graders. Cost for running the model on the entire subset is given in USD. Full confidence intervals are given in CC.4
Results shown Table 2
GPT-5
achieves the highest judging accuracy: 89.3%
with a single evaluation pass, approaching the 90.4% human baseline, and 90.8% with jority voting. Notably, OPC-R1-8B matches GEMINI-2.5-PRO'S majority voting perfor- mance and outperforms its base model by 17%, demonstrating the value of the OPC and its po- tential for advancing the field of proof evalu- ation and generation. However, the train for OPC-R1-88 shares the same distribution as this test set, which may inflate perfor- mance. In $C we show that while the perfor- mance OPC-RI-SB is reduced under out- of-distribution data, the improvement over the base model persists even under these condi- tions.
Judge
pass @
maj@5
Cost
HUMAN
90.4
N/A
GPT-5
89.3
90.8
117.77
GROK-4
88.3
89.8
104.42
GEM
85.4
88.
135.47
OPC-R1-8B
83.8
88.1
N/A
04-MINI
83.8
85.3
29.57
83.1
84.3
93.30
GEMINI-2.5FLLASH
82.7
86.0
86.95
OWEN3-233B-A22B
81.8
84.6
3.79
80.9
82.6
27.70
RI-QWEN3-8B
70.7
71.3
N/A
CLAUDE-4-SONNET
70.6
75.0
28.21
QWEN3-8B
64.4
63.6
N/A
GPT-4.1
61.4
60.8
20.33
This positive result appears to contradict Petrov et al. (2025), who reported poor performance of limited set of problems, relied on older
judge models. However, their evaluation was based models, and focused on the more challenging task of scoring proofs on a continuous rather than a binary scale. In addition, we put considerable effort into crafting clear and comprehensible prompts.
Self-evaluation LLMs often favor their own generations (Panickssery et al. 2024). To in- vestigate this, we evaluate how well models judge their proofs compared to those gener- ated by others. In Table [ we find that all models except OWEN3-235B-AR worse when judging their own proofs. This sug- gests that LLMs struggle to recognize their own mistakes, which is critical limitation for appli- cations requiring eeflluaaltiio.
Table 3: Judgement accuracy breakdown, high- lighting the lowest score for each judge. Full con- fidence intervals are given in SC.4
Judge
perform
GEMINI
04
QWEN
Prover
GEMINI
79.4
86.9
85.9
80.0
04
87.1
81.3
84.8
81.9
03
91.6
83.1
76.9
79.1
QWEN
80.6
84.1
87.8
84.4
5.3 FORMAL PROOF GENERATION LAGS BEHIND
Using the PutnamBench subset, we compare formal and natural language The best formal model, SREDEL-PRRVER-- (Lin et al. 2025b). achieves less than 19% accuracy on the PutnamBench. In contrast, Fig. shows that the top informal model, GEMINI-2.5 2.5-NN--..5PP- reaches almost 83% accuracy the evaluated subset, clearly outperforming this baseline. Despite this disparity. formal proofs offer a major advantage: automatic verifiability. While informal meth- ods currently dominate, formal approaches remain crucial for scalable proof verification.
models.
8

---

Published as a conference paper at ICLR 2026
60%
55%
Passen
Discrete
40.0%
uor
45%
Rank (Bracket)
Rank [Swiss]
40%
31.5%
32.9%
22.7% 7%
35%
20%
25%
2
0%
pass@1
Discrete
Continuous
Rank (Swiss)
(a) Pass versus all other best-of-n methods.
(b) Selection of methods on a larger subset.
Figure 6: Performance of the best-of-n selection strategies.
Finally, we note that recent private agentic system, Seed-Prover (Chen et al. (025). obtained a 50% formal accuracy on the PutnamBench. However, our informal results do not use agentic techniques, and it is therefore not accurate to directly compare these numbers.
5.4 PROOF GENERATION AND FINAL ANSWER Do NOT ALIGN
Although is widely claimed that final-answer benchmarks are inadequate for evaluating proof gen- eration capabilities (Petrov et al., 2025: Mahdavi et al.) 2025 Guan et al. 2025). it remains unclear how often LLMs can produce a valid proof when they find the correct answer. To investigate this, first collect instances from the MathArena subset where models generate correct final answers, and then manually evaluate the validity of the accompanying proofs. This enables us to estimate the overall proof correctness rate and compare it with the final-answer accuracy.
Results In Fig. 5 we report each model's final-answer accuracy alongside the stricter metric re- quiring valid proof. Despite DEMINI-2.5-PReS 04-MINI, and 03 achieving similar final-answer accuracy, proof correctness differs significantly. Specifically, 03 performs notably worse, with only 59.5% of its answers containing correct proof. This substantial difference between models shows that final-answer accuracy is not reliable indicator of proof generation capability.
5.5 BEST-OF-N SIGNIFICANTLY IMPROVES PERFORMANCE
Best-of-n selection strategies Best-of-n selection, generating multiple outputs and selecting the best one, is common strategy to improve performance. We evaluate this approach using 04-MINI by generating eight proofs per problem in the best-of-n subset and testing four selection methods:
Discrete: 04-MINI classifies each proof correct or incorrect and selects any correct one.
Continuous: 04-MINI scores proofs a 0-7 scale and selects one with the highest score.
Rank (Bracket): A ranking method proposed by Liu al. (2025). Proofs judged pairwise by MINI in a knockout tournament until one proof remains.
Rank (Swiss): Inspired by Liu al. (2025), proofs are paired in Swiss round-robin tournament. Ratings are computed using the Bradley-Terry model (Bradley and Terry 1952), and the proof with the highest rating is selected. See $ for details.
Prompts for all methods can be found in
Complexity Note that Rank (Bracket) requires (n)) comparisons, making it efficient as the discrete method, while Rank (Swiss) requires (n?)) comparisons, making more expensive.
Results on small subset In Fig. 6(a) we compare the performance of these methods with the pass@n metric on the 60 problems that contain human judgments for all eight proofs. We find that best-of-n selection strategies can significantly improve proof generation performance. Furthermore, the pairwise ranking methods outperform the discrete and continuous methods by approximately 10%. Notably, while discrete and continuous methods plateau after 5, ranking approaches continue scale. Finally, Rank (Swiss) slightly outperforms Rank (Bracket) by a 3% margin.

---

Published as a conference paper at ICLR 2026
Results larger subset In Fig. 6(b) strategies on the 134 problems of the best-of-n subset of the OPd" except for the Rank (Bracket) method, which was not evaluated methods is confirmed on the entire best-of-n subset, with Rank (Swiss) improving accuracy by 17%. While the confidence intervals problem set, all selection methods rely on the same underlying answers from 04-MINI, making the relative performance differences significant.
evaluate the performance of the best-of-n selection
the full subset. The improved performance of the ranking
relatively large due the small number of problems in this
5.6 POTENTIAL IMPACT OF CONTAMINATION
Since many OPC problems are publicly available, there is possibility that some were contaminated during training. In this section, we briefly explain why this plays an insignificant role in our results.
Proof generation capabilities In $C present small experiment indicating that contamination has a smaller effect than problem difficulty. Nevertheless, cannot be fully ruled out. In particular, the small gap in performance between GEMINI-2.5-4 and 04-MINT in $ cannot be conclu- sively attributed to genuine performance differences. However, results on smaller, contamination- 2025 Balunović al. (2225) also show GEMINI-2.5 outperforming
free datasets (Petrov 04-MINI, supporting the interpretation that the performance gap is real.
In all other sections, the conclusions are robust contamination: the informal-formal gap is too large to be affected by small changes, the discrepancy between final-answer accuracy and proof cor- rectness based on problems from MathArena, well-known benchmark with problems created in 2025, and best-of-n strategies are compared using the same model, making contamination irrelevant.
Proof judging capabilities Data contamina- tion poses a less significant risk for proof judg- ing, since generated proofs cannot present in the training data. The underlying problems and their official solutions, however, may have been during training, which could give models an advantage. To test this, we run a worst-case experiment where the ground-truth solution is provided alongside the proof to be judged. As shown in Table 4 the resulting accuracy gains are small and non-significant, suggesting that access to the solution does little to improve er- ror detection and that contamination has lim- ited impact on judging performance.
Table 4: Model accuracy with and without pro- viding the ground truth solutions. shows the change in accuracy between the settings.
pass I (w/ Solution)
Judge
GPT-5
89.3
89.0
-0.3
GEMINI-2.5-PRO
85.4
82.7
-2.7
OPC-RI-SB
83.8
83.1
-0.7
04-MINI
83.8
85.2
+1.4
03
83.1
85.9
+2.8
QWEN3-235B-A12B
81.8
84.9
+3.1
RI
80.9
80.8
-0.1
RI R1-QWEN3-8B
70.7
75.4
+4.7
LIMITATIONS
While the OPC represents a significant advancement in the development and evaluation of LLM proof-generatinn capabilities, it is not without limitations. First, since dataset construction took place before the release of GROK-4 and GPT-5, these models are only included as judges. How- ever, recent benchmarks suggest that these models perform similarly, perhaps slightly better, com- pared to GEMINI-2.5-PP conclusions. Second, the majority of problems in the OPC are derived from high-school competi- tions. Thus, the dataset does not cover more advanced mathematical domains, such as research-level mathematics. We further outline potential directions for expanding the OPC in
(Balunović et al. 2025). Therefore, it does not affect the validity of our
7 CONCLUSION
In this work, we introduced the Open Proof Corpus (OPC), a human-validated dataset comprising over 5,000 --ggenrrrteed proofs. Using the OPC, we addressed several open questions in the field, including (1) the gap between natural language and formal proof generation, (2) the relationship between final-answer accuracy and proof correctness, and (3) the effectiveness of best-of-n selec- tion. We also trained a model that achieves 88. 88.1% accuracy in judging proof correctness, matching GEMINI-2. 2.5-PRO and approaching the performance of the top model, GPT-5.
A small bug in the Rank (Swiss) method caused incorrect selections for 18 questions. These excluded from the analysis.
10

---

Published as a conference paper at ICLR 2026
REPRODUCIBILITY STATEMENT
We have included our dataset in the supplementary material, along with detailed descriptions of our methodology and experimental setup to ensure full reproducibility. addition, we provide our code with step-by-step instructions in the supplementary material, enabling others to replicate our results and for finetuning judge model. The dataset and judge model are also open-sourced in our HuggingFace repository, with clear documentation to facilitate use by the research community.
ACKNOWLEDGEMENTS
This work has received funding from the Swiss National Science Foundation (SNSF) 20000112079667] the Ministry of Education and Science of Bulgaria (support for INSAIT, part of the Bulgarian National Roadmap for Research Infrastructure), and the Swiss State Secretariat for Education, Research and Innovation (SERI).
REFERENCES
Alon Albalak, Duy Phung, Nathan Lile, Rafacl Rafailov, Kanishk Gandhi, Louis Castricato, Anikait Singh, Chase Blagden, Violet Xiang, Dakota Mahan, and Nick Haber. Big-math: large-scale, high-quality math dataset for reinforcement learning in language models, 2025. URL https:
//arxiv.org/abs/2500 17387
Mislav Balunović, Jasper Dekoninck, Ivo Petrov, Nikola Jovanović, and Martin Vechev. Math- arena: Evaluating Ilms on uncontaminated math competitions, February 2025. URL
https:
//matharena ai/
Ralph Allan Bradley and Milton Terry. Rank analysis of incomplete block designs: The method of paired comparisons. Biometrika, 396--4)3324-455, 12 1952. ISSN 0006-3444, doi: 10.1093/ Nlomet/39.3-4.333
htt.htttss//do..orgg/ttt http:////...1.////mtttt//////// 4.44.324
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma. Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang. Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang. Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, and Thomas Hanwen Zhu. Seed-prover: Deep and broad reasoning for automated theorem proving, 2025. Uttphttss:
//arxiv.org/ hatgg//bb//55555 23726
Alexis Chevalier, Jiayi Geng, Alexander Wettig, Howard Chen, Sebastian Mizera, Toni Annala, Max Jameson Aragon, Arturo Rodríguez Fanlo, Simon Frieder, Simon Machado, Akshara Prab- hakar, Ellie Thieu, Jiachen T. Wang, Zirui Wang, Xindi Wu, Mengzhou Xia, Wenhan Xia, Jiatong Yu, Junjie Zhu, Zhiyong Jason Ren, Sanjeev Arora, and Danqi Chen. Language models sci- ence tutors. In Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024. OpenReview.net. 2024. URL htttps://openreviee.nnnt net wwwtte/ooouoooee fwrm//orrmmm?a idd= WFFoonFZOR
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Refichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. CoRR, abs/2110.14166 2021. URL
http:://aaraiv.or/ab////// 14168
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In CADE, volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021.
Jasper Dekoninck, Maximilian Baader, and Martin Vechev. Polyrating: A cost-effective and bias-aware rating system for LLM evaluation. In The Thirteenth International Conference Learning Representations, ICLR 2025. Singapore, April 24-28, 2025, OpenReview.net, 2025. URL htt.:p/s//ooeeeeeeeeeeee/oo////s

---

Published as a conference paper at ICLR 2026
Simon Frieder, Luca Pinchetti, Alexis Chevalier, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Petersen, and Julius Berner. Mathematical capabilities of chatgpt. In Al- ice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neu- ral Information Processing Systems 2023, NeurlPS 2023, New Orleans, LA, USA, Decem- ber 10 - 16, 2023, 2023. URL http:://apperrt wwpppppppp.....pp.ppppppppppppsm www.pps.ccpappr.r.. Abwtrrattt
551666882294556663333333633 a www.dddeccaarrss...o html
Bofei Gao. Feifan Song, Zhe Yang. Zefan Cai, Yibo Miao, Qingxiu Dong, Lei Li, Chenghao Ma, Liang Chen, Runxin Xu, Zhengyang Tang, Benyou Wang, Daoguang Zan, Shanghaoran Quan, Ge Zhang, Lei Sha, Yichang Zhang, Xuancheng Ren, Tianyu Liu, and Baobao Chang. Omni- math: A universal olympiad level mathematic benchmark for large language models. In The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net 2025. URL httpss://oppeereviee wor/f wttp://wwwww...ooomooooocaaaaoaa
Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Car- oline Falkman Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, Olli Järviniemi, Matthew Barnett, Robert Sandler, Matej Vrzala, Jaime Sevilla, Qiuyu Ren, Elizabeth Pratt, Lionel Levine, Grant Barkley, Natalie Stewart, Bogdan Grechuk, Tetiana Grechuk, Shreep- ranav Varma Enugandla, and Mark Wildon. Frontiermath: A benchmark for evaluating advanced mathematical reasoning in AI. CoRR, 00//2211..448772 2024. URL httts:tts/////i.orrr org/ 48550/ 24...
doi: 10.48550/ARXIV.244 1.0472..
Jiawei Gu, Xuhui Jiang, Zhichao Shi. Hexiang Tan, Xuehao Zhai, Chengjin Xu, Wei Li, Yinghan Shen, Shengjie Ma, Honghao Liu, Yuanzhuo Wang, and Jian Guo. A survey on llm-as-a-judge. CoRR, 0bbs/2411.15599) 2024, doi: 1044550ARXXV.2411.55555 URL https:://oii.rrg// 48850/arXivv 111..151994
Xinyu Guan, Li Lyna Zhang, Yifei Liu, Ning Shang, Youran Sun, Yi Zhu, Fan Yang, and Mao Yang. rstar- math: Small Ilms can master math reasoning with self-evolved deep thinking. CoRR, abs/2501.04519, 2025. doi: 10448550/RRXV22500.666 04519. URL WRLLhttps://// https: httt:::/ddoi.org/11 wttp//..g/////// 48556/
Daya Guo, Dejian Yang, Haowei Zhang. Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-rl: Incentivizing reasoning capability in Ilms via reinforcement learning. arXiv preprint 1XXi:22501.12945 2025a.
Jiaxing Guo, Wenjie Yang, Shengzhong Zhang, Tongshan Xu, Lun Du, Da Zheng, and Zengfeng Huang. Right is not enough: The pitfalls of outcome supervision in training Ilms for math rea- soning. 2025b.
wwtp:////5/.......////////// 06877
Chaoqun Hc, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Leng Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, Jie Liu, Lei Qi, Zhiyuan Liu, and Maosong Sun. Olympiadbench: A challenging benchmark for promoting AGI with olympiad-level bilingual multimodal scientific problems. In Lun-Wei Ku, Andre Martins, and Vivek Srikumar, editors, Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Vol- ume 1: Long Papers), ACL 2024, Bangkok, Thailand, August 11-16, 2024, pages 3828-3850. As- sociation for Computational Linguistics, 2024. doi: 118653/V1/20244AALLLL https://doi.orge: org/10...111... 18653/11/2224....
URL
Long.211 2111
Zhiwei He, Tian Liang, Jiahao Xu, Qiuzhi Liu, Xingyu Chen, Yue Wang, Linfeng Song, Dian Yu, Zhenwen Liang, Wenxuan Wang, Zhuosheng Zhang, Rui Wang. Zhaopeng Tu, Haitao Mi, and Dong Yu. Deepmath- 103k: A large-scale, challenging, decontaminated, and ver- ifiable mathematical dataset for advancing reasoning. CoRR, abs/2504.11456 2025. doi: 10.48550/ARXIV.2504. 1456. URL htttps://t/o.ii.. www.:ii..rgr...... 4855000/55////xii 25444..1.6.
Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed Ki-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, Alex Iftimie, Alex Karpenko, Alex Tachard Passos, Alexander Neitz, Alexander Prokofiev, Alexander Wei, Allison Tam, Ally Bennett, Ananya Kumar, Andre Saraiva, Andrea Vallone, Andrew Duberstein, Andrew Kondrich, An- drey Mishchenko, Andy Applebaum, Angela Jiang, Ashvin Nair, Barret Zoph, Behrooz Ghor- bani, Ben Rossen, Benjamin Sokolowsky, Boaz Barak, Bob McGrew, Borys Minaiev, Botao
12

---

Published as a conference paper at ICLR 2026
Hao, Bowen Baker, Brandon Houghton, Brandon McKinzie, Brydon Eastman, Camillo Lu- garesi, Cary Bassin, Cary Hudson, Chak Ming Li, Charles de Bourcy, Chelsea Voss, Chen Shen, Chong Zhang, Chris Koch, Chris Orsinger, Christopher Hesse, Claudia Fischer, Clive Chan, Dan Roherts, Daniel Kappler, Daniel Levy, Daniel Selsam, David Dohan, David Farhi, David Mely, David Robinson, Dimitris Tsipras, Doug Li, Dragos Oprica, Eben Freeman, Eddie Zhang, Ed- mund Wong, Elizabeth Prochl, Enoch Cheung, Eric Mitchell, Eric Wallace, Erik Ritter, Evan Mays, Fan Wang, Felipe Petroski Such, Filippo Raso, Florencia Leoni, Foivos Tsimpourlas, Francis Song, Fred von Lohmann, Freddie Sulit, Geoff Salmon, Giambattista Parascandolo, Gildas Chabot, Grace Zhao, Greg Brockman, Guillaume Leclere, Hadi Salman, Haiming Bao, Hao Sheng, Hart Andrin, Hessam Bagherinezhad, Hongyu Ren, Hunter Lightman, Hyung Won Chung, Ian Kivlichan, Ian O' O'Connell, Ian Osband, Ignasi Clavera Gilaberte, and Ilge Akkaya. Openai ol system card. CoRR, 117222 2024. doi: 1048550AARXIV.2112.67777 URL http:://doi.org/////// wtt.:////////.../////aaoo/ 48550/arXiv
2412. 16720
Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample. and Stanislas Polu. Numinamath. cattuuu..ommppooo///// prwjecttnnmiiiee aimo aimo- hww.greess.prieeebb/////////eeee hataaaiaaannaannttaaaaaaaaaaa dataset.pdf), 2024.
[https://huggiiggaace
Hunter Lightman, Vincet Kosaraju, Yuri Burda, Harrison Edwards. Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net, 2024. UtL/httss:///oenneeee wttp://wwww.t.eooo/mmd/////o////
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover: frontier model for open- open-source automated theorem proving. CoRR, Abss2250.006640) 2025a. doi: 00.48550/ARXIV.252.0000 URL https:///oi..rgg// 48554048555//aii. ww...5552200770
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang. Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction, 2025b. URL httpp:
//arxiv.org/aae
63613
Yantao Liu, Zijun Yao, Rui Min, Yixin Cao, Lei Hou, and Juanzi Li. Pairjudge r:: Perform best-of-n sampling with knockout tournament, 2025. URL
13007
Hamed Mahdavi. Alireza Hashemi, Majid Daliri, Pegah Mohammadipour, Alireza Farhadi, Samira Malek, Yekta Yazdanifard, Amir Khasahmadi, and Vasant G. Honavar. Brains vs. bytes: Evaluating LLM proficiency in olympiad mathematics. CoRR, abs/2504.01995, 2025. doi:
10.44850/ARXXI225044000
URL. htttp:::::oi.org///ooo hrt.:///0oro1.1..////rrr//. 2504. 01995
Philipp Mondorf and Barbara Plank. Beyond accuracy: Evaluating the reasoning behavior of large language models A survey. CORR, abs/2404.011669, 2024. doi: 10.48550/ARXI..444.001
URL htttps://t/.i.... org. 11w.1..885585rxix.. http///xxxvv...44... 01869
Ivan Moshkov, Darragh Hanley, Ivan Sorokin, Shubham Toshniwal, Christof Henkel, Benedikt Schifferer, Wei Du, and Igor Gitman. AIMO-2 winning solution: Building state-of-ther the- math- ematical reasoning models with openmathreasoning dataset. CORR, abs/2504. 1 6891, 2025. doi:
10.48550/ARRIV22500 16891. URL httt:::s//d:oooorg// wttp://r/.....55/rr/aa.... 48550/arXiv 2504. 16891
Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002.
OpenAl. Openai o3 and 04-mini system card, April 2025. URL https://cdn www.ai.ennnncc....e comppdf/ 2221c875 87777588822--788--9 100s--80bb-ee0 3722bbe27777332211333333 and 04 mini- www.yttteeadddd.r.
Arjun Panickssery, Samuel R. Bowman, and Shi Feng. LLM evaluators recognize and favor their own generations. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Pa- quet, Jakub M. Tomezak, and Cheng Zhang, editors, Advances in Neural Information Processing
13

---

Published as a conference paper at ICLR 2026
Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024,
Vancouver, BC, Canada, December 10 15, 2024, 2024. URL | http://ppppppr...s....ppp ccpps.cpppppppprrrrr
Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav
Balumovic, Nikola Jovanovic, and Martin Vechev. Proof or bluff? evaluating Ilms on 2025
USA math olympiad. CoRR, abs/2503.21934, 2025. doi: 10.4850/ARXXV.220222229 URL
48550/arXiv, https://doi.org// / wttp5///.w.iv.......... 21933
Qwen Team. Qwen3: Think Deeper, Act Faster, April 2025. URL https://qwenn.. wwwhubthhh...... io/
blog/qwen3/ Qwen Blog.
Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseck-prover-v2. prover-v2: Advancing formal mathe- matical reasoning via reinforcement learning for subgoal decomposition. CoRR, abs/2504.21801, 2025. doi: 10-8550/ARXXIV2544210011 21801
URL. httt::://doi.orr/100 wtt..///.0.805////11...00000
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. CoRR, htbs/2402.03300 2024. doi: 10.4550/ARXXV.2402..055
URL
https://doi. 4wt.....55//ariii 2462 83300
Guangming Sheng, Chi Zhang, Zilingfeng Ye, Xibin Wu, Wang Zhang, Ru Zhang, Yanghua Peng, Haibin Lin, and Chuan Wu. Hybridflow: A flexible and efficient rlhf framework. arXiv preprint arXiv: 2409. 2024.
Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, and Pan Lu. Solving inequality proofs with large language models, 2025. URL.
07927
Parshin Shojace, Iman Mirzadeh, Keivan Alizadeh, Maxwell Horton, Samy Bengio, and Mehrdad Farajtabar. The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity, 2025. URL//tttss//aarx...rr//////////
Gemini Team. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long
context, and next generation agentic capabilities. CoRR, abs/2507.06261 2025. doi: 10.48550/ ARXIV.2507.06261 URL https::///oi.orr/111 48550/.88588888 arxiv 2w0.
George Tsoukalas, Jasper Lee, John Jennings. Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem- provers on the putnam mathematical competition. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, ed- itors, Advances in Neural Information Processing Systems 38: Annual Conference on Neu- ral Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, Decem- ber 10 15, 2024, 2024. URL http::/ nips wwtpppppppeppeeeeccc.cceeeee. fillss/paerr2282//aaah 1552eafeecct390eeeeeeee533333333
Abstract Datasets and Benchmarks. www.rssttss.nnn..ennnnrsk.r..... Track. html
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang. Zhilin Yang, Zhengy- ing Liu, and Jia Li. Kimina-prover preview: Towards large formal reasoning models with re- inforcement learning. CoRR, abs/2504. 1354, 2025. doi: 10.48550/ARXIV.504.1 13354. URL https://doi.orge: wtt.:////....///...i...... 2564. 11354
XAI. Grok 3 beta - the age of reasoning agents, February 2025. URL htL.ittps///x..aaeew//rrr Accessed: 2025-04-03.
14

---

Published as a conference paper at ICLR 2026
Shijie Xia, Xuefeng Li, Yixin Liu, Tongshuang Wu, and Pengfei Liu. Evaluating mathemati- cal reasoning beyond accuracy. In Toby Walsh, Julie Shah, and Zico Kolter, editors, AAAI- 25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 March 4, 2025, Philadelphia, PA, USA, pages 27723-27730. AAAI Press, 2025. doi:
https///s:///oi www.:i...rg11... 1609/ aaa9//aaai.00 v39126.................. 34987
Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, and Weiyang Liu. For- malmath: Benchmarking formal mathematical reasoning of large language models, 2025. URL.
https://arxiv.org/ aww//ba//..... 02735
Hugh Zhang, Jeff Da, Dean Lee, Vaughn Robinson, Catherine Wu, William Song, Tiffany Zhao, Pranav Raja, Charlotte Zhuang, Dylan Slack, Qin Lyu, Sean Hendryx, Russell Ka- plan, Michele Lunati, and Summer Yue. A careful examination of large language model performance on grade school arithmetic. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, UIrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors, Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, Decem- ber 10 15, 2024, 2024. URL http:///apers: mipppperssiiis....mmm..p wwtppss.ccpppp...eee filles/paper/2224/nas)) $3384ff990ca55ccc2c$$$8888
Abstract- Datasets.aaaaetts....m and_ Benchmarks. Tranaaakksssrkrr....e Track. html
Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang. Qiuzhi Liu, Yansi Li, Linfeng Song, Zhenwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, and Dong Yu. Deeptheorem: Ad- vancing Ilm reasoning for theorem proving through natural language and reinforcement learning, 2025. URL https:///axxi http://wwwii..rr///////./.// 23754
Chenyan Zhao, Mariana Silva, and Seth Poulsen. Autograding mathematical induction proofs with natural language processing. CoRR, 102668 2024. doi: 10.48555ARXXV.2266.1022
URL https://6o1.org//1 http:/rggg.....//rrrii..... 2406. 10268
Chenyan Zhao, Mariana Silva, and Seth Poulsen. Language models are few-shot graders. In Alexandra I. Cristea, Erin Walker, Yu Lu, Olga C. Santos, and Seiji Isotani, editors, Artificial Intelligence in Education 26th International Conference, AIED 2025, Palermo, Italy, July 22- 26, 2025, Proceedings, Part IV, volume 15880 of Lecture Notes in Computer Science, pages 3-16. Springer, 2025. doi: 0100077978-33031-9855555 978-3- 031 98459-4_1
URL https://66o..rrg/0...k
Kunhao Zheng. Jesse Michael Han, and Stanislas Polu. minif2f: cross-system benchmark for formal olympiad- mathematics. In The Tenth International Conference on Learning Representattins, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL
https:://openreview.no http::/wwww......oooooooo/oeoore
Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. Judging ilm-as-a-judge with mt-bench and chatbot arena. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, edi- tors, Advances in Neural Information Processing Systems 36: Annual Conference on Neu- ral Information Processing Systems 2023, NeurlPS 2023, New Orleans, LA, USA, Decem- ber 10 16. 2023, 2023. URL http::/papers..rtt//////// .nippperrs..sssi.immm www.:iii.s.pcpprrr.eeeppppppp wwtpppcpppppppppcppetccceeec...p Seaerrfflee filess/pper/20223/aas
15

---

Published as a conference paper at ICLR 2026
Table A list of competition sources for the problems in OPC.
Competition
Description
Probicms Solutins
Level
Type
Ace
Source
Ralkan MO
Comprition betwor Balkan
31.256
Ralli: Way
Norhhm Funopean Olympiad Finl the Olympial
Prelininary sound
Olympptdd
Uriganan Competitions
Compettoon:
Itulganaa grade)
Earoopaa
hurope-wod dlympad univer
only girls perticipnnss
Shottist
Shocilist problens. which IMO
18.0%
Internaiooal Zharrsoo MO
Kazakastan based
questious
MO
Pinal
trio Ulymptdd
Pacssan
Undergrdaat aanaaaaalle compettioon. regandal
the most diflical
UG
100,0%
Romaniat Minters Matherazics Extrlist
IMO-llvel competitoon hosted Romanie
33
162
135
43.39
Swiss MD
Varioss problens from the Swiss Olympiad
8
135
$7.5%
PuMi
USA Junicr MD USAMO
USA olympaal thee allmes only pinve stndems
121
H55
Pontec
The findl rand the USA Math Olyngial
190
H5
35.19%
Putnamllench
aduute competttoon ropanded the diticult
MathArena
ATME 2025
Anvecr-bacal competitonn
qualiter for USAMO
24
155
N
95.7%
Pybhic
BRUMO 2025
Anvecr-beccll competiion bosted Boww Univerityy
28
114
155
M
100,05
HMMT Pobeaoy 2025 SMT 2025
Answer bosed compention hosted Harvart and MLT
26
103
135
N
97.81%
PORKR
Saswer-bosed compettion bosted Stanfred
34
1280
115
92.016
Best-af-n
Cumpeition countrics
jeobleus, Olympiad
A COMPETITIONS THE OPC
The OPC contains over 1000 problems that were sourced from national and international competi- tions of varying difficulty. In T we present the problem and sample distribution for each. We also include the following additional information:
Level: the education level the problems appropriate for, either high school (HS) or undergraduate (UG).
Type: whether the competition is hosted internationally (I) or only nationally (N).
Source: link the source from which we obtained the problems. Any source that is publicly available was marked as "Private".
Ace: the average accuracy of the best best-performing model on the competition problems, which serves as rough proxy for difficulty.
B SWISS RANKING METHODOLOGY
We briefly describe the Swiss ranking method used as best-of-n selection strategy. In this approach, a round-robin tournament performed where each proof competes against every other, In each "game", proofs compared by 04-MINI, which decides which proof is better, or if they equally good.
To determine the overall winner, compute rating for each proof using the Bradley-Terry model (Bradley and Terry 1952). , a probabilistic model for paired comparisons commonly applied in LLM evaluation (Zheng al. 2023 Dekoninck al. 2025). The Bradley-Terry model estimates the probability that a proof with rating r; beats a proof with rating ry as:
1
P(i beats
1 exp(ri ri)
We fit the model to the outcomes of the round-robin toumament using maximum likelihood esti- mation, resulting in a rating for each proof. The proof with the highest rating is selected as the best.
16

---

Published as a conference paper at ICLR 2026
Table LLMs as proof graders on undergraduuate-evel problems. Cost for running the model on the entire subset is given in USD. Confidence intervals are 95% and computed using the large sample normal approximation.
Judge
pass @
maj @
Cost
04-MINI
83.8 3.1
85.1 + 2.9
48.31
GPT-5
8.1
+4.03.0
89.42
R1
78.3
79.7 3.3
51.86
OPC-RI
75.0
77.0 3.5
N/A
RI-QWEN3-8B
72.1 3.7
72.4
+ 3.7
N/A
-EMINI-2.5-PRO
70.9 3.8
76.7
+ 3.5
160.95
100%
89 93%
833 9%
83,65
100%
84.7%
81.2%
78,8%
80%
60.3%
60%
40%
20%
20%
0%
Number (b) Problems are binned in the four main categories: Algebra, Combinatorics, Geometry, and Number Theory.
Algebra
Combinatorics
056
(a) Problems binned difficulty level, with higher levels indicating more challenging problems.
Figure 7: Influence of difficulty level and problem category the prevalence of incorrect proof's in MrthArena.
C ADDITIONAL RESULTS
In this section, present further results, specifically addressing critical aspects of our evaluation: out-of-distribution performance of our trained model and the potential impact of data contamination.
C.I OPC-RI-8B PERFORMANCE OOD PROBLEMS
During the training of OPC-RI-SB, our dataset primarily consisted of samples from high-school level competitions, aligning with the distribution of the set. Crucially, undergraduate-level prob- lems were explicitly excluded from training. To evaluate OPC-RI -88'ss generalization capabilities dittr--iiittibuttion data, evaluated its judging performance 560 undergraduate-level solu- tion samples sourced from the Putnam competition.
As shown in Table 6. OPC-R1-8B retains notable improvement over its base model, despite undergraduate-level examples not being present in its testing set. While frontier models like 04- achieve higher performance, OPC-R1-S is nevertheless competitive, performing on par with GEMINI-2.5-PHe This shows that the OPC data can be applied to mathematical domains beyond its scope.
C.2 PROBLEM CATEGORY AND DIFFICULTY AFFECT INCORRECT PROOF RATES
We analyze the prevalence of incorrect proofs in the MathArena subset of the OPC. In particular, we investigate whether difficulty and problem type correlates with the likelihood of model gener- ating an incorrect proof. As shown in Fig. 7 we find that both these factors significantly influence performance. In particular, higher difficulty levels correspond to greater proportion of incorrect proofs, as illustrated in Fig. (a) Additionally, among the four main problem categories, Geometry problems exhibit the highest rate of incorrect proofs.
17

---

Published as a conference paper at ICLR 2026
Standard Competitions
Non aon--ttaddard competitions
$0.7%
411%
18.2%
22.1%
18.9%
15.5%
20%
0%
Gemini-Pro
6.
o4-mini
Qwen3
R1
Grok-Mini
XI
Figure 8: Average proof correctness sample of the OPC, split into Standard and Non-standard
competitions.
C.3 DATA CONTAMINATION FOR MATHEMATICAL PROOFS
Test-set contamination prevalent challenge in evaluating the true reasoning capabilities of mod- els, particularly in mathematics (Balunović et al. 2025 Zhang et al. 2024). Given that the vast majority of OPC problems are publicly sourced, conduct one additional experiment address potential contamination-relatee concerns.
Competition-based breakdown First, outline 2 categories of competitions: Standard and Non-standard. The former includes important competitions in the mathematics community, namely the IMO Shortlist and USAMO. Problems from these widely recognized competitions more likely to appear in training sets, as they are widely reported on the internet and therefore represent the greatest potential risk for contamination.
On the other hand, the Non-standard category consists of problems from the International Zhau- tykov Olympiad, the Swiss Mathematical Olympiad, and the Bulgarian seasonal competitions. A significant portion of these problems required translation from their original non-English statements, and they originate from less prevalent sources compared the IMO and USAMO. Consequently, we anticipate a substantially lower prevalence of contamination within this problem set.
As illustrated in Fig. g model accuracy on Standard problems notably lower than on their Non- standard counterparts. This observation indicates that problem difficulty is considerably more dominant factor influencing model performance than the potential presence test-set contamina- tion. While this experiment alone cannot definitively discount the presence of test-set contamination within the OPC dataset for our $5.1 results, it demonstrates that the models' wrolemmssolving ca- pabilities extend significantly beyond memorization. This suggests that any contamination effect is likely small and not the primary driver of performance differences.
C.4 SIGNIFICANCE ANALYSIS
In Table we present the performance of various LLMs as proof judges, along with 95% confidence intervals using the large sample normal approximation. In Table we provide detailed breakdown of judging accuracy by prover, again with 95% confidence intervals. These tables complement the main results presented in $
D EXPERIMENTAL DETAILS
In this section, we provide additional details regarding our experimental setup, including model training, hyperparameters, and evaluation protocols.
18

---

Published as a conference paper at ICLR 2026
Table 7: LLMs proof graders. Cost for running the model on the entire subset is given in USD. Confidence intervals are computed using the large sample normal approximation.
Judge
pass @ 1
maj @5
Cost
HUMAN
90.4 + 3.4
N/A
GPT-5
89.3 + 3.5
90.8 3.3
117.77
GROK-4
88.3 3.7
3.5
104.42
GEMINI-2.5-PRO
85.4 4.0
8.7
135.47
OPC-RI-8B
8.2
88.1
N/A
04-MINI
8.2
8.1
29.57
8.3
4.2
93.30
GEMINI-2.5-FLASSH
82.7
8.0
86.95
QWEN3-235B-A22B
4.4
8..6
3.79
R1
4.5
4.3
27.70
R1-QWEN3-8B
5.2
5.2
N/A
CLAUDE-4-SONNET
70.6
5.0
28.21
QWEN3-8B
64.4 5.5
03.6
N/A
GPT-4.1
61.4 5.6
60.8 + 5.6
20.33
Table Judgement accuracy breakdown by prover with 95% confidence intervals.
Judge
Gemini
04
03
Qwen
Prover
GEMINI
79.4 + 4.9
86.9 + 4.1
85.9 + 4.2
80.0 = 4.9
04
87.1 4.1
81.3 = 4.8
84.8 4.4
81.9 4.7
03
91.6 3.4
83.1 4.6
7.2
79.1 = 5.0
QWEN
80.6 4.9
84.1 + 4.6
87.8
84.4 4.5
D.1 MODEL TRAINING
Training data As outlined in $ we split the generic split of the OPC dataset into a train and test The training set consists of 1,733 proof samples, while the test contains 293 proof samples. Importantly, we ensure that no problem statements overlap between the training and test sets, maintaining the integrity of our evaluation.
Reinforcement learning We fine-tune RI RI-QWEN3-8B using GRPO (Shao et al. 2024) on the training set using the popular VERL. framework (Sheng et al. 2024) with learning rate 10-6 maximum response length of 14000 tokens, 10 rollouts per problem, and batch size of 16. We use the same prompt for training as for evaluation, as shown in [.3] More hyperparameters and training details can be found in the provided code. Importantly, we did not use the test set any point during training or hyperparameter tuning, and only evaluated the final trained model once on the test set.
D.2 MODEL. EVALUATION
Hyperparameters and prompt For all models, use the recommended hyperparameters out- lined by the model providers. For open models, this usually involves using nucleus sampling with p 0.95 and temperature of 0.6. For closed models, we use the default settings provided by the API. Model-specific hyperparameters can be found in the provided code. Prompts used for evalua-
tion are shown [
Formal model performance To accurately compute the performance of GOEDEL-PROVERS V2 (Lin et al. 2025b) on our subset of problems from T'suuaalas et al. (002)), we contacted the authors of the models to obtain the raw results for each problem. This allowed us to compute the exact accuracy on our selected problems, which was not reported in the original paper.
19

---

Published as a conference paper at ICLR 2026
E QUALITATIVE OBSERVATIONS
Building on our quantitative analysis, we present several qualitative insights drawn from our judges' evaluations. These include common failure modes and notable model behaviors.
Incorrect handling of inequalities Many models sometimes make mistakes when manipulating inequalities. frequent issue the improper reversal of inequality signs during intermediate steps without mathematical justification. This results in incorrect final answers despite seemingly coherent reasoning. Below is example of such mistake made by RI, where the incorrect sign reversal is marked with "**"
Baltic Way 2004 P3
...
Sunming these inequalities gives
Eg 9+h 2 Exe (1 3c05)133) =3 =3- Eo
...
again,
1/3 + 61/3 2/3 Vat/3p///22// 3(abe) 1./0
equality only 2/3 84/3 62/3, 1.e.,
atb+r
Struggles with synthetic geometry reasoning Olympiad-level geometry problems, models often default to coordinate-based methods, i.e., using computations with complex numbers spe- cific coordinate system to "bash" the problem, especially on easier problems where such techniques tractable. However, for harder problems, models tend shift toward synthetic approaches, lying on geometric theorems and properties. These harder problems typically require keeping track of multiple different but related angles and robust understanding of geometric relationships. Here, models frequently struggle: they sometimes confuse angle orientations, misidentify congruent an- gles, reverse point orderings, or apply geometric properties incorrectly. In the following example, GEMINI-2255PP5 correctly identifies the base of an isosceles triangle in one case, but subsequently deduces the wrong pair equal iigulss-illutrraiingg a common mngle-reasoning failure.
GEMINI-2.5-PRO IMOSL 2013 G4
Thus, LPBA = LQBA Mhere these angles are L(BP, BA) and L(AB, BQ). The problen states these are equal 7.
So. L(BP, BA) = and L(AB, BQ) = 7. This reans LPBQ= L(BP, BA) (AB BQ) =7 27.
D interior point segnent BQ PD PB.
Thus, APBD isosceles triangle
BD.
The angle LPBD APBD is LPBQ, so LPBD 27.
The base angles are
LBPD LBDP
180
90
LPDB 90
Since segnent
L(DP, DB) -0
Incorrect citation of IMOSL 2004 G8 by GEMINI-2.5-PRO A curious behavior observed exclu- sively in GEMINI-PRO is the repeated and inappropriate citation of the 2004 IMO Shortlist geometry problem G8. This reference appears in over 15 different solutions, often in problems unrelated to
20

---

Jury and Published as a conference paper at ICLR 2026
geometry. Notably, these citations consistently at points where the model appears to get stuck. No other model in our evaluation displayed this behavior. An illustrative example is shown below.
EGMO 2018 P3
contestants
C1, Cz....,
competition, they queue
restaurant according to the following rules.
The chooses the initial order of the contestents the queue.
Every minute, the Jury chooses an integer with g &&S n.
contestant
other contestants front
pays her, restaurant opens
roves forward in the queue by exactly positions.
contestant process ends.
For
that this can collect by cunningly chousing the initial order and the sequence of moves.
terninate and determine the maximut number of that the Jury
GEMINI-2.5-PRO
The problen
that the always terminates find naxinun number the Jury can collact. One euro is callected for each move contestant makes.
have two relations:
k- for each == 1....... (positional balance for each Ck).
Σe-1 k- Eh-1je je (total junp events balance).
Substitute (1) into (2):
Lk= my _x= my).
This equation is an Identity and does not help itself.
Let the argunent fron ISL 2004 68 solution notes:
The of positions Se Pk n(n 1)/2, which constant.
The costs, km (position of C+) k.
Overgeneralization from simple cases Consistent with prior work (Petrov et al. 2025 Mahdavi et al. 2025), we observe that models often overgeneralize patterns from small or simple examples. This tendency leads to incorrect solutions, particularly when the identified properties do not extend to the general case. An example illustrating this pattern overreach is included below.
Ø GROK 3 MINI IMO SL 2000 G4
Let A142As be an acute acute-angled triangle. Denote the feot of the altitude from vertex A, to the side appnsite As Ks, and the where the incircle touches the side opposite A, Iis The Lines Ki K2 K2 Kg. and Ky are the sides of the arthic triangle, and the Lines I, I2 IgTa, and Lign are the sides of contact triangle.
the special case of equilateral triangle, the orthic triangle and contact triangle coincide, the reflections result in the Lines, with vartices the incircle. For general acuto-angled triangle, coordinate geonetry calculations in specific exanptes (e.g., triangle with vertices at B(0, 0), C(4, 0), A(1, 2)) confim attributable rounding errors.
intersection points lie
incircte,
Given the symettr of the configuration and the properties the incircle as the unique circle tangent to the sides, the intersection points P. Q, and lie the incircte for any acute-angled triangle. Thus, triangle forned by Mis, Mag, and Mat has vertices incircle.
F FUTURE WORK
The OPC offers a valuable resource for advancing research in proof generation with LLMs, sup- porting both the training and evaluation of models for this task. Our analysis also highlights several critical gaps and challenges that require further research. First, the significant disparity between formal and natural language proof generation shows the need for more effective strategies to bridge
21

---

Published as a conference paper at ICLR 2026
this gap. Second, the OPC shows that current benchmarks fail to capture the full complexity and quality of generated proofs as they often rely solely on final answers. Therefore, the development of scalable benchmarking pipeline tailored to proof generation tasks is necessary. Finally, while our results show that best-of-n sampling strategies can meaningfully improve proof quality, further research is required to better understand and optimize these methods.
G STATEMENT FOR THE USE OF LARGE LANGUAGE MODELS
Beyond being the subject of research, LLMs were used only assistants to improve the clarity and quality of writing. They were not involved in aiding our research methodology, ideation, or for discovering related work.
H GRADING INTERFACE AND INSTRUCTIONS
This appendix outlines the grading interface and the accompanying instructions provided to judges. The full interface and documentation can be accessed and reviewed in our supplementary material.
Judge ID Each judge received unique identifier, which served as their login credential on our website. This ID was used to track grading progress while maintaining judge anonymity in the resulting dataset. To facilitate discussion and resolve ambiguities, a shared communication channel was created between all judges.
Grading interface The grading interface was designed for clarity and ease of use. Figs. 1 illustrate its main components. The left panel contains navigation bar for switching between problems and competitions. The right panel displays the problem statement and the ground-truth solution, along with options for flagging issues either. Below, the generated solution is shown, accompanied by an automated summary and potential issues identified by an LLM judge. Judges can then evaluate the solution using a grading form that allows them to:
Indicate whether the solution correct or incorrect
Provide brief justification
Highlight specific parts of the solution relevant to their decision
Indicate uncertainty or abstain from grading
Instructions Judges received a set of guidelines detailing how to use the interface and evaluate the correctness of solutions. Of partieular importance the criteria for determining whether a proof should be marked correct:
Instructions for judges when proof is correct
would Se/7 points full grading. Examples of snall penalties worth 1 point are if the solution:
solution should be considered correct
Nakes corputational nistake
easily fixed Nisses an edge case which can be easily proven/disproven without such reasoning
Skips over step
A solution should be narked as incorrect if: marks step trivial, if It onits algebra-heavy conputational steps, regardtess of whether or not it has outlined the nethodology Generalizes pattern without rigorously describing pattern, without proving any relevant properties.
innediately abvinus why this would be the
eei-tiistiig unpopular source/Thearen, it online. Thus, theorens that can be innediately found and have Mikipedia article are allowed
cannet imediately
searching
The nodel has specifically told that it should skip steps of this rule should be considered by assuning the model does not know how to derive the "trivial" step.
then trivial. Any violation
These instructions were developed collaboratively with the judges and refined iteratively based on their feedback, ensuring consistent grading across different problems and evaluators.
22

---

Published as a conference paper at ICLR 2026
Apntrod
Figure 9: Main grading interface. The left panel provides navigation across problems and competi- tions. The right panel displays the problem and ground-truth solution, with options to report issues.
Figure 10: Interface for evaluating generated solution. The problem repeated for reference. The generated solution appears on the left, and the LLM's summary and identified issues on the right.
Figure 11: Grading form. Judges indicate correctness, provide justification, highlight relevant content, and optionally express uncertainty or abstain.
23

---

Published as a conference paper at ICLR 2026
I PROMPTS
In this section, we provide the prompts used for various tasks in the OPC. The prompts designed to be clear and concise, guiding the LLMs through the proof generation process while ensuring that they understand the requirements for correctness and clarity. In $1.II we present the prompts used for generating proofs. In $1.2 we provide the prompt used to generate the LLM summary to aid human graders in identifying potential issues in the proof. $1.3 we present the prompt used for we provide all prompts used
LLMs to judge the correctness of proof, used in 5.2 In $ L.7
S.7
for the LLMs in best-of-n sampling, as described 5.5
1.1 PROOF GENERATION PROMPT
The following prompt is used for problems with no final answer:
Prompt
Your task 1s write proof solution to the following problen. Your proof will be graded by human judges for accuracy, thoroughness, and clarity. When you write your proaf, follow these guidelines:
You are creating proof, not proof outline. Each step shoutd be carefutly explained and docurented, If not progerly explained, judge assure you cannot explain it, therefore decrease your grade.
use general theorens lemas, only they are well-knoun. fanous enough to have Wikipedia allowed. Any result from papers that would not he taught in high school or Low-level bachelar courses in used.
result has nate
or sonething similar to describe it, It is
wathenatics
results irmediately give Do not skip conputation steps in your preof. Clearly explain what tramstontsionss were done and why they step calculation.
grade,
are
You should use correct LaTeX notation to urite equations and nathenstical synbols. You should encorpass these equations in appropriate synbots ("M" and "WI for intine math, "W!" and "WI block math) enhance the clarity of proof. not any unicode characters.
Your proot should be fof-cootaieed.
prove intermediate state this. It is nuch preferable to indicate your uncerteinty rather than naking incorrect staterents or
you
specific step,
clearly
(problen)
The following prompt used for problems with a final answer:
Prompt
folloving problen. proof for accuracy, thoroughness, and clarity. When you write proaf, follow these guidelines:
proof
by hunan judges
You creating proof, not proof outline. Each step should be carefutly explained and docurented. not properly explatned, the judge will assune that you cannot explain it, and therefare decrease your grade.
You can use general theorens and lemas, but only if they are well-known. As rule of thunb: if the enough have Wikipedia page or something allowed. Any result from papers that would not be taught in high school or Low level bachelar courses in nathematics should
result
describe it, it
used. Any use of such results will inmediately give you zero grade. skip conputation steps in proof. Clearly explain what transfomations are allowed in each step of calculation. LaTeX
done and they
equations nathenatical synbols. should encorpass these equations in appropriate synbuls ("V"" and "W\ for inline nath, "W! and "W" for block nath) any unicade characters.
should use
elarity your proaf. Your proof should be seLf-contained.
you are not sure about specific step, or not know hav to prove an intermediate result, clearly state this. nuch preferable indicate uncertointy rather than naking incorrect staterents clains.
your final answer Wbboeed(()).
(prablen)
24

---

Published as a conference paper at ICLR 2026
1.2 ISSUES INTERFACE PROMPT
Prompt
help hunan nethenatician proof will write surnary of the provided proof and highlight patential issues with it.
given probler. task, you
one Input:
input will consist
following components:
>*Problen Statements>; A natheratical problen that the proof is attempting to solve. **Ground-Truth Solution-e: available,
correct solution to problen, reference. Note that ground truth solutions moy not always be pravided, can alsa contain nistakes, and are often overly succinct. The ground-truth proof is nainly provided to help you understand the problen better. orissions,
xsProof Salution=>: The proof that need evaluste. This may contain unclear steps. The proof was generated by another language rodel, which was givan the following instructions:
-nodel_pronge
carefully explained docurented. not properly explained, the judge will assure that cannot explain it, and therefare decrease your grade.
creating proof, proof
step
You general theorens lemas, only if they well-knoun. As rule of thumb: the resalt has a nare and is fanous anough to have a Wikipedia page or somothing similar to describe it, it is Any
papers that would rathenstics should not be used. Any use of such results will inmediately give you zero grade.
taught high school low-level bachelor
in done and why they
skip conputation steps your proof. Clearly explain what transfomations are allowed in each stop of calculation.
You should use correct LaTeX notation to write equations and nathenatical synbols. You should encorpass these equations appropriate symbols ("W" and "WI for inline "WI" and "WI block math) enhance the clarity of your proot. Do not use any unicode characters. should self-contained.
If you are not sure about specific step, or do not know haw to prove an internediate result, clearly preferable indicate your uncortainty rather naking incorrect staterents or
state
clains.
</modell.poop
AN Surnary Guidelines:
First, should write concise surmary of the proof solution. The surnary should capture the main ideas exhaustive. goal to provide clear everview
and steps the proaf, but what the proof is attenpting to accorplish. A surmary should consist only few sentences, and it should not contain any judgnent or evaluation of the should purety descriptive.
not
Issues Highlight:
Your main task identify potential issues proof salution. should include any and all issues that can find, no watter how small. Here are sone comron types of Issues to look for: ==Dvergenerliizationn. The generated proof proceeds by proving the probler in one or more specific cases holds generat. Hovever,
then concludes case.
provide proot the general
without proper justification. Highlight any and all stops that are marked as trivial or abvinus, even if you think they are indeed trivial.
#xbversiimllficaaioon::::
steps
v*Skipping Corputation Stepsex; Proofs that skip computation steps not explain transfornations clearly can lead to nisunderstantings. Highlight any steps where the proof skips necessary calculations or explanations.
<xciting Non-Standard Works or Theorenses: Sone nodels nay cite theorens or results that are not well- known or not typically taught high school allowed if they are well known. If the proot cites such results, highlight this as potential issue, even you think it is justified.
bachelor courses. thearers are only
edge cases. If notice that the proof does not address certain scenarios, highlight this as patential issue.
veHissing Edge Cases-e; The proof nay consider all possible
weirang Final Answerve:
proof arrives final that incorrect, highlight
potential issue. *+0thoram: Any
above categorics but you believe significant
enough to be hightighted.
For each of these the issue, and indicate the category of the issue.
should identify where in the proof they provide brief explanation
If there are nore than four issues, you should onl highlight the four rost significant anes. Sort the issues by their significance, with the nost signi ficant issue first.
d*# Additional Instructions:
Do not provide final grade or score for the proof. Your task is to sumarize and highligght potential evaluate the proot
25

---

Published as a conference paper at ICLR 2026
critical thorough your analysis. you find issues, you probably look closely enough.
you are unsure decide.
something an issue,
to highlight
grader
Use clear and concise language in your sumrery and issue descriptions. The goal your response is to add work for then. The clear concise your
help
huran grader's work, response is, the better it will be for the hunan grader. LaTeX
equations and nathenatical synbols your You should encorpass these equations in apprapriate synbels ("VM" and "W" for intine math, "W" and characters.
You
"WI block nath)
clarity your proof.
any "W" for single backslash.
all syrbols in output JSON, For exemple, Spend special attention to producing valid JSON, It needs be parsable by standard JSON parser.
Properly
#84 Output Format:
Fornat your reply using JSON object follows:
*>* jssn
"surnary": cancise surmary of solution.", "Issues":
"location": "A description of where the issue occurs in the proof".
"text": citation excerpt
issue. issue is very snall part of the proof (e.g., single sentence), you leave this field enpty.",
proof
"description": "A brinf explanation of the issun.", "category"; "The category of Steps, Citing Hon-Standard Works or Theorens, Missing Edge Cases, Mrong Final Answer, 0ther)." 11,
(Overgeneralization, oversinpliiication, Skipoing Corputation
you truly find any you erpty array erpty list).
(prablen)
éa Fround-Truthh Solution:
(ground truth. solution)
### Proof Solution: soluof.solution)
1.3 LLM JUDGE PROMPT
Prompt
You are judging the correctness of LUN-generated preof for nath problen.
#zd Input:
Your input will consist the following components:
<<Prablen Staterent=>:; A notheratical problen that the proof is attempting to solve. you evaluate. unclear steps. The proof was generated by another language nodel, which was given the following
-*Proof Solutione>;
may contain errors, orissions,
instructions:
<nodel. pronpt>
You are creating proof, not proof outtine. Each step should be carefutly explained and docurented,
not properly explained, the will assure that cannot explain it, and therefore decrease grade.
You
general theorens lemas,
if they well-known.
of thunb: the
result has nare and is fanous enough to have Wikipedia page or something similar to describe it, it is allowed. Any result
taught high school wathenatics should not be used. use of such results will irmediately give zero grade. not skip conputation steps in your proof. Clearly explain what transfomettons were done and why they calculation.
papers
would
bachelar courses
allowed each
You should use correct LafeX natation to write equations and mathenstical synbols. You should encorpass for inline "WI and "WI block nath)
appropriate symbols ("W(" enhance the elarity of your proaf. Do not use any unicade characters.
proof should self-contained.
not sure about specific step, not know haw to intermediate result, clearly state this. is nuch preferable to indicate your uncerteinty rather than naking incorrect staterents or clains.
</nadel_pronpt>
26

---

Published as a conference paper at ICLR 2026
solution A solution should be considered correct even if it would earn 5+/7 points in standard grading format. Exarples snall penalties
graded:
point Nakes small corputational nistake that
easily fixed Nisses an edge case which can be easily proven/disproven
Skips
that fallows without nuch reasoning nanual work
Depending on the severity and the context, you ma also not penalise given error. On the other hand, narked It narks step as trivial, if it is not innediately obvieus with little reasoning why this would be the case.
solution
onits algebra-heevy conputational steps, regardless of whether not it has outlined the nethodology. Skipping sharter computations should be pernitted.
Generalizes pattern without rigorously describing the pattem, without proving any relevant properties.
searching it online. Thus, theorens that can be innediately found and have Mikipedia article are allowed.
non-existing unpopular
cannet imredistlly
The nodel has been specifically told that it should skip nark then trivial. Any violation this rule should be considered by assuning the model does not know how to derive the "trivial" step.
MN Scoring instructions
If you believe the proof is carrect, end your analysis with (coore((())rreet). If you believe the proof is incorrect, and your analysts with (tnearr())))))))))))
##e Problen Statoment: (problen)
Solution:
(salution)
1.4
LLM AS JUDGE PROMPT WITH GROUND TRUTH SOLUTION
Prompt
You judging correctness LUN-generated proof problen.
Input:
Your input will consist the following components:
**Problen Statemente=; natheratical problen proof attempting
.+Ground Truth Solution-e; The solution of the problen, as originally written by the probten's authors. may contain errors, orissions, or
you evaluate. unclear steps. The proof was generated by another language rodel, which was given the following
Solutiones:
instructions:
<node <rodee_pronpt>
You are creating proef, not proof outline. Each step should be carefutly expleined and decurented. you explain it, therefore
properly explained, judge grade.
your
Lemas, only they are well-known. result has nare and is fanous enough to have Wikipedia taught in high-school low-level bachetor courses in used. Any use of such results will innediately give zero grade. Do not skip conputation steps in your proof. Clearly explain what transfomations were done and why they calculation.
general
ar something similar to describe it, it is
allowed. Any result from papers that would
vathematics should
You should use correct LaTeX notation to write equations and nathenatical synbols. You should encorpass nath, "W" "W] enhance the clarity of your proot. Do not use any unicade characters.
these equations appropriate synbols ("W" "Wi
math)
Your proof should be self-contained.
know haw to intermediate result, clearly state this. It is nuch preferable to indicate your uncertainty rather than naking incorrect staterents or clains.
not about specific step,
</model__proppt>>
*Nd How the solution should be graded:
A solution should be considered correct even if would earn 5+/7 points in standard grading fomat, Exarples of snall penalties worth point
the solution:
Nakes snall corputational nistake that can rasily fixed edge
which Skips over a step that fallows without such reasoning or ranual work
easily proven/disproven
Depending on the severity and cantext, you may alse not penalise given error. other hand, solution should be narked incorrect if:
It narks a step as trivial, 1f it not innediately obvious with little reasoning why this would be the
It anits algebra-hman heavy conputational staps, regardless of whether or not it has autlined the nethodol Skipping shorter computations should pernitted.
27

---

Published as a conference paper at ICLR 2026
Generalizes pattern without rigorously describing pattern, without proving any relevant properties.
searching online. Thus, theorens that can be innediately found and have Mikipedia article allowed
non-existing unpopular source/lheoran
cannet imedistely
The nodel has specifically told that it should of this rute should be considered by assuntng the model does not know how to derive the "trivial" step.
steps then trivial. violation
#he Scoring instructions
believe the proof correct, end analysis with (eboeed((ooreect).. If believe the proof incorrect, end your analysis with (inarrt()).
#8 Problen Staterent:
(problen)
(gt.solution)
Model Solution:
(solution)
1.5
LLM DISCRETE JUDGE PROMPT
Prompt
judging correctness LUt-generated
problen.
Input:
Your Input will consist the following components:
*4Prablen Statementem: nothenatical problen that proof attempting to solve.
**Proof Solution=>; The proof that you need to evaluate. This proof may contain errors, orissions, or steps. proof generated by
language
was given following
instructions:
prongt>
You are creating proof, not proof outtine. Each step should be carefutly explained and docurented. not properly explained, the judge will assure that you cannot explain it, and therefore decrease your grade.
You can use general theorens and lemas, but only if they are well-known. As rule of thunb: if the enough have Mikipedia page or something low-level
describe it, allowed. Any result from papers that would not be taught in high school law: level bachelar courses in nathenatics should
result
used. Any use not skip conputation steps in proot. Clearly explain what transfomations are allowed each step calculation.
results
imeediately give you zero grade.
done and they
equations nathenatical synbols. should encorpass these equetions in appropriate synbols ("WM" and "\\" for inline neth, "W! and "W' for block nath) to clarity your proof. Your proof should be celf-contained.
should
LaTeX notation
any characters.
you are not sure about specific step, or state this. is ruch preferable indicate uncertainty rather than naking incorrect staterents or clains.
haw to prove internediate result, clearly
prompt>>
solution
graded:
A solution should be considered correct even 1f it would earn 5e/7 points in standard grading format Exarples of snall penalties worth 1 point are the solution:
easily fixed Nisses an edge case which can be easily proven/tisproven
Nakes snall conputational, nistake that
Skips step that fallows without such reasaning nanual work
Depending on the severity and the context,
ray also not penalise given error. On the other hand,
solution should narked incarrect
marks step as triviat, 1f it not innediately obvious with Little reasoning why this would be the case.
onits algebra-hewe heavy conputational, steps, regardless of whether not it outlined the nethodology. Skipping sharter computations should be permitted.
Generalizes pattern without rigorously describing the patter,, without proving any relevant properties.
non-existinng unpopular source/Thearen, cannet imediately found searching online. Thus, theorens that can be innediately found and have Mikipedia article allowed
##t Further Potential Issues:
types Look
28

---

Published as a conference paper at ICLR 2026
abvergeneralization:: The generated proceeds by proving and then concludes that the result holds in general. Hovever, it does not provide a proof for the general
specific
trivial obvious without *skipping Corputation Stepsax; Proofs that skip corputation steps or not explain transiornations clearly lead misunders
The proof narks
justification.
+eCiting Non known ton-Standard Norks or Theorensee: Sore rodels may cite theorems or results that are not wett- typically taught high school low-level bachelor courses. allowed if they are well known.
are only possible cases edge cases.
weHissing Edge Cases-e: proof may
The nodel has been specifically told that it should not skip steps or mark then as trivial. Any violation this rule should considered assuning the rodal does not know how derive the "trivial" step.
Scoring instructions
you believe proof carrect, your analysis (coore((carrrec)). you the proot incorrect, end analysis with (incrr).......ee)))...
Problen Statement:
(problen)
*** Model. Solution:
(salution)
1.6 LLM CONTINUOUS JUDGE PROMPT
Prompt
You are judging the correctness of LLM LUN-generated proof for a math preblen.
#** Input:
input will consist
following component::
**Problen Statementsw; & natheraticcal probten that the proof is attempting to solve.
may errors. orissions, unclear steps. The proof was generated by another language rodel, which was given the following instructions:
Solutione<:
you
<node
You are creating proof, not proof outline. Each step should be carefutly explained and decurented. you explain it, therefare decrease your
properly explained, judge grade.
general result has nare and is fanous enough to have Wikipedia ar soncthing similar to describe it, it is allowed. Any result papers
lenras, only they well-known.
taught high school low-level bachelar courses wathematics should not used. Any use of such results will innediately give zero grade. Do not skip conputation steps in your proof. Clearly explain what framsionntionss were done and why they calculation.
would
You should use correct LaTeX notation to write equations and nathenatical synbols. You should encorpass nath, "W" "WI block enhance the clarity of your proof. Do not use any unicade characters.
these equations appropriate synbols ("W"" "Wi
Your proot should be self-contained.
not sure about specific step, not know how to intermediate result, clearly state this. It is nuch preferable to indicate your uncertainty rather than naking incorrect staterents or
</nodel_pronpt>
and How the solution should be graded:
A solution shoutd be graded out of total of points. Exarples of snall penalties worth point are if the solution:
Nakes snall corputational nistake that can rasily fixed which Skips over a step that follows without such reasoning or ranual work
Nisses edge
easily praven/dlsproven
Depending on severity
cantext, you may also ponalise given error. other hand, poor grade if:
solution should receive It waars a step as trivial, 1f it not innediately obvious with Little reasoning why this would be the
It onits algebra algebra-heavy conputational stops, regardless of whether or not it has autlined the nethodology. Skipping shorter computations should pernitted. Generalizes aver pattern without rigorously describing the pattem, without praving any relevant properties.
It cites non-existing unpoputar source/Theoren, which cannot be immediatlly found fron searching for it online. Thus, any theorens that can be innediately found and have a Mikipedia article are allowe.
The nodel has been specifically told that it should not skip steps ar mark then as trivial, Any violation considered by assuxtng the nodel does know derive the "triviat" step.
29

---

Published as a conference paper at ICLR 2026
#H Further Potential Issues:
Here corrin types of issues look for:
=#vergeneralization--s The generated proof proceeds by proving the probler in one or nore specific cases Howover, it does not provide praof for the general
and then concludes that the result halds in case.
without proper justification. *eSkipping Corputation Stepsix: Proofs that skip computation steps or do not explein transfornations risunderstandings.
*#Oversinoliiication
steps trivial
clearly
<<Citing Non-Standart works or Theorens Sone nedels nay cite theorens results that not well- known or are not typically tought in high school or lov-level bachelor courses. Such thearers are only allowed if they well
**Missing Edge Cases-e; The proof nay not consider all possible cases or edge cases.
##d Scoring instructions
Your should be number between and 7, where the proof completely incorrect, and the proaf is completely correct. Be very critical in your grading. If you find snall errors, deduct points accordingly.
Output
your analysis, present your grade number between and
Problen Staterent: (problen)
#* Model Solution:
(solution)
1.7 LLM AS RANK JUDGE PROMPT
Prompt
You are judging which of the two LUN-generated proofs for given nath problen is better.
*84 Input:
input
following components:
<>Problen Statement>>; & natheratical problen that the proof is attempting to solve.
Solution A/B-e; proofs you unclear steps. Proofs were generated by another language madel, which was given the fallowing instructions:
proof may contain errors, onissions,
<node <rodet_prongt>
You are creating proef, not proof outline. Each step should be carefutly explained and decurented. it, therefore
properly explained, judge grade.
you
your
general result has nare and is fanous enough to have Wikipedia ar something similar to describe it, it is taught in high school low-level bachelor courses in used. Any use of such results will innediately give Do not skip conputation steps in your proof. Clearly explain what transfomations were done and why they calculation.
lemas, only they well-known.
allowed. Any result from papers that would
vathematics should
grade.
You should use correct LaTeX notation to write equations and nathenatical synbols. You should encorpass nath, "W" "WI enhance the clarity of your proot. Do not use any unicade characters.
these equations appropriate synbols ("W" "Wi
math)
Your proof should be self-contained.
know haw to intermediate result, clearly state this. It is nuch preferable to indicate your uncertainty rather than naking incorrect staterents or clains.
not about specific step,
prompt
eNd How the solution should be graded:
The following examples are snall nistakes that should only slightly penalised:
Makes snall corputational, nistake that
easily fixed
Nisses an edge case which can be easily praven/disprovmn step
fallows without such reasoning On the other hand, solution should should be severely penalised if: marks step as trivial, 1f not innediately abvinus with reasoning why this would case.
Skips
work
It onits algebra-heavy conputational steps, regardless of whether or not it has outlined the nethodology. Skipping sharter computations should permitted. Generalizes aver pattern without rigorously describing the patter,, or withaut proving any relevant properties.
30

---

Published as a conference paper at ICLR 2026
unpopular source/Theoren, It online. Thus, any theorens that can be innediately found and have Mikipedia article are allowd.
inrediately
searching
The nodel has been specifically told that it should not skip steps or nark then trivial. Mn violation this rule should be considered by assuning the model does not know how to derive the "trivial" step.
684 Further Potential Issues:
Herr are some consen types of issues to look for: -*Overgeeerllizatiimee:
generated proof procceds by proving probles and then concludes that the result holds in generat. Hovever, it dees not provide proof for the general case.
more specific cases
*4Dversinpls inceatiootiiaaiion- The proof narks staps trivial abvious without proper justification. +*Skipping Computation Stepsee; Proofs that skip corputation steps or do not explain transfornations nisunderstendings.
clearly
<sciting Standard Works or Theorensen: Sone nodels may cite theorens or results that are not well- bachelor courses. thearers are only
know not typically taught high school
allowed if they well known.
**Missiing Edge Cases The proof may not consider all possible cases or edge cases.
*A Scoring instructions
You should conpare the two proofs and determine which one is better. If you believe Proof is better, and your analysts ((bxedd((A)) you Proof better. your analysts (())) you believe both proafs equally good, your analysis with (equi)()
Probien Statement:
(problen)
##d Proof Solution A: (solution_a)
##d Proot Salution B: (solution.b)
31


Reviews:
[{"review_id": "wIfB4bDJRP", "reviewer": "Reviewer_C4Eu", "summary": "The authors introduce a set of approximately 1000 contest math problems, drawn from existing competitions, whose LLM proof is humanly rated (binary), to be used both as an eval set and training set. They use the dataset to assess how correct the proof is compared to the (correct) final answer. The dataset, as a training dataset, is validated by fine-tuning an 8B R1-Qwen model, which is claimed to match GPT5.", "questions": "N/A", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "The problem assessment pipeline is rigorous. \n\nThe single fine-tuned model on OPC is a welcome addition that supports OPC. \n\nThe dataset size is sufficiently large to allow finetuning.", "weaknesses": "- misleading statement: my biggest issue is that apparently not the full dataset was shared, as only USAMO and BMOSL seem to appear in the zipped supplementary (and also for these, not the full dataset? seems quite small), contrary to the claim: \"We have included our dataset in the supplementary material, along with detailed descriptions of our methodology and experimental setup to ensure full reproducibility.\"\n\n- ambiguous claim: \"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.\"\nAs it reads, it is unclear if the authors claim to be the first ever to create such a dataset, or the first to create such a dataset in the more narrow domain of contest math problems (only the latter is correct). Since this is from the **appendix**, I would urge the authors to rewrite.\n\n- missed important prior literature: Probably the first paper on \"pure\" autograding was https://arxiv.org/abs/2406.10268, and there is (rather similar) follow-up work by these authors https://arxiv.org/html/2502.13337v1  (it would be good to include this in the related work section). But much earlier work exists implicitly in ML even if not marked as autograding, e.g. in 2024 https://arxiv.org/abs/2402.11111 a more detailed methodology for \"LMs as evaluators\" was derived (see also more papers on prior such literature), or **2021** in the well-known paper https://arxiv.org/abs/2110.14168, which used what they called \"verifiers\" All this points to an existing body of work on proof judging that is missing from this paper.\n\n- Wrong claim: \"Data contamination poses only a minor risk for proof judging, since generated proofs cannot be present in the training data.\"\nI am unsure on what information this claim rests - who is to say that the main LLM companies don't exactly do this? They have their LLMs generate outputs on contest-level problems to ensure that their LLMs can potently act as judges, which can be of use for subsequent pipelines that the companies might use, or in case the public wants to use LLMs as judges, and companies are interested in having their LLMs perform well on publicly known problems. This seems entirely plausible to me, so I believe this statement should be retracted.\n\n- in terms of the results, with some exceptions, the paper seems to reinforce known folklore beliefs about how models performance on mathematics.\n\n- Almost no details are given about fine-tuning on R1 Qwen3-8B. In particular, rivalling the performance on GPT-5 is a dubious claim (presumably a heldout subset of OPC was used for this on which R1 Qwen was not train? details are missing)", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "tkE5ZoRYzP", "reviewer": "Reviewer_J7sP", "summary": "This paper introduces the Open Proof Corpus (OPC), a dataset of 5,062 LLM-generated mathematical proofs across 1,010 problems from prestigious competitions (IMO, USAMO, Putnam), each evaluated by human judges. Using the OPC, the authors demonstrate: (1) informal proof generation outperforms formal by 4x on PutnamBench, (2) significant gaps exist between final-answer accuracy and proof correctness (especially for o3, dropping from 87.6% to 59.5%), and (3) ranking-based best-of-n strategies achieve 47% accuracy versus 26% pass@1. They also fine-tune an 8B model that achieves 88.1% accuracy in judging proofs, approaching GPT-5's performance.", "questions": "- Why binary labels? Could you release the raw judge feedback to enable partial credit analysis? This would be valuable for understanding proof quality gradients.\n- Model failure modes: The observation that only 114/1700 incorrect proofs acknowledged uncertainty is striking. Could you analyze whether this varies by problem difficulty or type?\n- Formal proof training: Have you considered fine-tuning informal models on formal proof data to better understand the performance gap?\nCompetition selection rationale: Was there systematic criteria for choosing these specific competitions over others (e.g., Putnam over Mathcounts)?\n- Extending beyond competitions: Have you considered including undergraduate textbook problems or research-level lemmas? What would be needed to extend OPC to these domains?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "- Addresses critical need: First large-scale dataset of human-evaluated LLM proofs, filling a major gap since existing benchmarks focus only on final answers (e.g., AIME, HMMT).\n- Methodology: Well-designed grading pipeline using 13 former IMO participants, clear guidelines, double-grading (90.4% agreement), and clever use of LLM-generated issue summaries to aid grading efficiency.\n- Significant empirical findings: The 4x gap between informal/formal proof generation and the divergence between answer accuracy and proof correctness are important insights. The ranking-based best-of-n showing 21% absolute improvement is practically valuable.\n- High-quality dataset design: Thoughtful splits (MathArena, PutnamBench, best-of-n, generic) enable targeted analyses while preventing test set contamination.", "weaknesses": "- Binary evaluation loses information: The \"5+/7 points counts as correct\" threshold is arbitrary and discards nuanced quality differences that partial credit scoring would capture.\n- Unfair formal/informal comparison: Comparing specialized formal proof models against general-purpose LLMs isn't apples-to-apples. The brief mention of Seed-Prover's 50% formal accuracy suggests the gap may be overstated.\n- Missing statistical analysis: No confidence intervals, significance tests, or error bars despite sufficient sample sizes.\n- Insufficient contamination analysis: Section C.2's comparison of \"Standard\" vs \"Non-standard\" competitions is suggestive but not conclusive. The performance differences could be explained by difficulty alone.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "VfngolkN9b", "reviewer": "Reviewer_LpED", "summary": "The paper presents large-scale dataset of high-difficulty math problems which includes both correct/incorrect proofs and profound annotations which are represented via human-expert judgements. Based on the dataset, some exciting insights are proposed.", "questions": "1. Can you clarify the guidelines used by judges for borderline proofs? How are omissions or shortcuts treated when deciding correctness?\n2. Could you provide more insight into common errors when models give correct answers but incorrect proofs? Are these mostly algebraic mistakes, logical gaps, or misapplied theorems?\n3. Does this discrepancy vary systematically by problem type or difficulty?", "limitations": "", "rating": 8, "confidence": 5, "soundness": 3, "presentation": 2, "contribution": 4, "strengths": "1. A fairly large dataset of math problems is proposed, with its core value lying in expert annotations. Furthermore, both correct and incorrect proofs are included. It is quite unusual for modern math benchmarks and datasets to contain such annotations, making this contribution valuable to the community.\n2. Some exciting empirical insights are provided. While I do not feel that the exploration of performance differences between natural and formal proof generation is particularly valuable, since the performance degradation in formal setups is largely expected, the examples illustrating the discrepancy between final-answer correctness and proof correctness are important.\n3. The performance of the fine-tuned, moderately sized LLM judge is impressive.", "weaknesses": "It might be somewhat subjective, but the presentation quality is low, even considering the number of figures included in the manuscript. While it is understandable that the authors tend to include more content rather than placing all figures in the Appendix, the text in each section is highly granular. I think this weakness could be addressed by rethinking the overall structure. The main focus should be on the dataset itself, which is valuable, while the incremental contributions in the form of interesting observations should either be explored more deeply or moved to the Appendix.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "OVk8C68Lz0", "reviewer": "Reviewer_kWHN", "summary": "In this work the authors curated a new dataset called the open proof corpus, which contains 5,062 LLM-generated proofs of 1,010 distinct problems from math contests. These proofs are all incorporated with manual reviews from human experts. They have also done a lot of researches around this dataset, especially on the proof judging capabilities of different LLMs.", "questions": "* How are the results in Table 2 (Section 5.2) evaluated actually? I did not find any further descriptions of the settings of these experiments around this chapter. If the performance of LLM judges is evaluated by comparing with human labels, then are they directly comparable with human baselines?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "* This work answers a lot of interesting questions in this area.  \n\n* This paper provides a comprehensive study on the proof evaluation capability of LLM, fulfilled an important blank in the research of AI4Math.", "weaknesses": "* The evaluation of proof judgement may be heavily dependent on the judger’s prompt or criteria, so neither the judging accuracy nor the alignment with human graders are accurate enough.  \n\n* This work did not cover problems from advanced math or research-level math, where proof problems weigh more importance than math competitions. This limits the contribution of OPC.  \n\n* The creation of this OPC heavily depends on manual annotation from experts, which limits the scalability of this work.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "QspVhn6pHH", "reviewer": "Reviewer_Ybod", "summary": "LLMs excel at math final-answer tasks (e.g., AIME) but struggle with rigorous proof generation—critical for research/theorem proving. Existing proof benchmarks are small, outdated, or closed, leaving 3 key questions unaddressed: (1) natural vs. formal proof gap, (2) final-answer vs. proof correctness link, (3) best-of-n strategy impact. Several findings are elaborated in the paper:\n- Natural language proofs outperform formal ones (GEMINI-2.5-PRO solves 4x more PutnamBench problems than top formal model).\n- Final-answer accuracy is not equal to proof correctness (O3 loses ~30% accuracy when proofs are required, vs. 8% for GEMINI-2.5-PRO).\n- Best-of-n pairwise ranking boosts accuracy significantly.\n- LLMs match humans in proof judging.\n- LLMs rarely admit uncertainty and struggle to judge their own work.", "questions": "See weaknesses.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- Rigorous proof generation/evaluation pipeline.\n- First large, open, human-validated LLM-proof dataset (OPC).\n- High-Quality Data: Expert judges (IMO background) ensure reliable labels; diverse, competition-sourced problems.\n- Actionable Insights: Quantifies critical gaps (natural vs. formal proofs) and validates best-of-n strategies.\n- Openness: OPC and code are open-sourced; transparent methodology for reproducibility. I think this will be a good resource in theorem proving area.", "weaknesses": "- Narrow Problem Scope: Most problems are high school-level (IMO/USAMO); few undergraduate/research-level tasks.\n- Outdated Provers: GROK-4/GPT-5 are only used as judges, not prover, which misses latest LLM proof capabilities.\n- Lack of analysis of why formal theorem provers lag behind natural language counterparts. This is an interesting comparison, it would be great if there can be some deeper analysis.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)