Official Review · ICLR 2026

This paper introduces a new benchmark to evaluate the performance of large language models on formal mathematical proving across various topics at the high school and undergraduate levels. It situates the work in relation to existing datasets, emphasizing the benchmark’s larger scale and broader topic coverage. The authors conduct empirical evaluations to analyze the weaknesses of current LLM-based provers and summarize several common error patterns. To ensure correctness and formal validity, the benchmark is constructed through a human-in-the-loop process involving both LLMs and human experts. The syntax of the generated problems is verified using Lean 4, the semantics are checked by other LLMs, and final validation is performed by human reviewers. ● The authors have made significant efforts to collect and compile a large set of mathematical proof problems for the proposed benchmark. The resulting dataset covers a much broader range of topics and difficulty levels than existing benchmarks, substantially extending the scope of the math-proving domain. ● The increased scale of the benchmark offers opportunities for further improving, fine-tuning, or post-processing LLMs for formal reasoning tasks. It also provides a convenient and comprehensive resource for researchers and practitioners interested in evaluating models across diverse mathematical areas and levels of difficulty. ● While I appreciate the authors’ effort to present detailed findings and observations from using the proposed benchmark to evaluate existing LLMs, very little information about the dataset itself is provided in the main paper. This limits the paper’s clarity and informativeness. It would be helpful if the authors included a brief discussion of the benchmark’s data format, data collection process, and implemented evaluation metrics. If space is a concern, the presentation of Table 2 could be optimized to make room for these essential details. ● Continuing from the last comment on information clarity, the description of the evaluation setup is missing in Sections 4 and 5, which makes the paper less self-contained without the appendix. A concise summary of the experimental configuration would improve readability and reproducibility. ● The paper points out that existing formal mathematics benchmarks are limited in scope, focusing mainly on a few high school or college-level topics. While I appreciate the broader coverage this benchmark brings, the paper should give stronger justification for the kind of depth and qualitative diversity it adds that’s beyond simply combining more problems. ● The benchmark mainly reports the Pass@K metric, which offers a limited view of performance. Adding other evaluation measures such as final proof accuracy, intermediate reasoning correctness, or step-by-step reasoning quality would give a more complete picture of model performance. ● In Figure 2, both the undergraduate and high school math domains include Precalculus. Are there any