---
title: "The Open Proof Corpus — paper by Dekoninck et al. (2025)"
description: "The authors build the Open Proof Corpus (OPC). 90.8% accuracy. 55 references, cited by 10 papers here."
authors: ["Jasper Dekoninck", "Ivo Petrov", "Kristian Minchev", "Mislav Balunovic", "Martin Vechev", "Miroslav Marinov", "Maria Drencheva", "Lyuba Konova", "Milen Shumanov", "Kaloyan Tsvetkov", "Nikolay Drenchev", "Lazar Todorov", "Kalina Nikolova", "Nikolay Georgiev", "Vanesa Kalinkova", "Margulan Ismoldayev"]
year: 2025
venue: "arXiv:2506.21621"
source: "https://arxiv.org/abs/2506.21621"
doi: "10.48550/arxiv.2506.21621"
arxiv: "2506.21621"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/dekoninck-2025-open-proof-corpus-large-scale/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/dekoninck-2025-open-proof-corpus-large-scale/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/8/) / The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs

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

**Authors:** [Jasper Dekoninck](https://md.research.elamur.ai/free/en/authors/jasper-dekoninck/), [Ivo Petrov](https://md.research.elamur.ai/free/en/authors/ivo-petrov/), Kristian Minchev, [Mislav Balunovic](https://md.research.elamur.ai/free/en/authors/mislav-balunovic/), [Martin Vechev](https://md.research.elamur.ai/free/en/authors/martin-vechev/), Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, Nikolay Drenchev, Lazar Todorov, Kalina Nikolova, Nikolay Georgiev, Vanesa Kalinkova and Margulan Ismoldayev · **Year:** 2025 · **Venue:** arXiv:2506.21621 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2506.21621) · [PDF](https://arxiv.org/pdf/2506.21621) · [DOI 10.48550/arxiv.2506.21621](https://doi.org/10.48550/arxiv.2506.21621) · [arXiv 2506.21621](https://arxiv.org/abs/2506.21621) · [OpenAlex](https://openalex.org/W4416260167)

**Citations:** 1 citations (OpenAlex, 2026-10-14) · [10](https://md.research.elamur.ai/free/en/papers/dekoninck-2025-open-proof-corpus-large-scale/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Progress in LLM-based proof writing is held back by the lack of a large, carefully graded collection of model-written proofs. Earlier proof evaluations are small, use outdated models, contain few valid proofs, or are not public. The authors build the Open Proof Corpus (OPC). Strong current LLMs attempt problems from elite competitions such as the USAMO and IMO, and human graders label each proof as correct or incorrect and add written feedback. A dedicated pipeline for problem preparation, grading and quality monitoring made it possible to annotate thousands of proofs in about four weeks.

Some problems come from PutnamBench and MathArena. This lets the data answer three questions:
- how informal proving compares with formal (Lean) proving;
- how often a correct final answer comes with a valid proof;
- how much best-of-n selection helps.

The results show that natural-language proving clearly beats formal provers. Correct answers often hide flawed proofs, and ranking-based selection gives large gains. Fine-tuning a small open model on the OPC produces a proof judge close to the best proprietary systems, which makes cheap automated grading more realistic.

## Key points
- The OPC contains over 5,000 human-judged LLM proofs for more than 1,000 competition problems, and about 43% of them are correct. O4-MINI solves nearly 20% of IMO Shortlist problems.
- GPT-5 judges proof correctness with 90.8% accuracy, roughly matching human graders. R1-QWEN3-8B, fine-tuned on the OPC with GRPO, reaches 88.1%, comparable to GEMINI-2.5-PRO.
- On PutnamBench, GEMINI-2.5-PRO solves about four times as many problems as the strongest formal prover, GOEDEL-PROVER-V2.
- Requiring a full valid proof costs GEMINI-2.5-PRO about 8% of its final-answer accuracy, while O3 drops by almost 30%.
- Standard best-of-n selection raises accuracy from 26% to 36%. A pairwise ranking approach, where an LLM compares two proofs, reaches 47%.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,450 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,296 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works

🧭 Topics (2): [🧠 Language models & pretraining](https://md.research.elamur.ai/free/en/topics/language-models/) · 3,894 works · [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works

## Cite

Cite as: Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin Vechev, Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, Nikolay Drenchev, Lazar Todorov, Kalina Nikolova, Nikolay Georgiev, Vanesa Kalinkova and Margulan Ismoldayev. 2025. The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs. arXiv:2506.21621.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{dekoninck2025open,
  title = {{The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs}},
  author = {Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin Vechev, Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, Nikolay Drenchev, Lazar Todorov, Kalina Nikolova, Nikolay Georgiev, Vanesa Kalinkova and Margulan Ismoldayev},
  year = {2025},
  doi = {10.48550/arxiv.2506.21621},
  eprint = {2506.21621},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2506.21621}
}
```

- [← previous SR-LLM: Rethinking the Structured Representation in Large Language Model](https://md.research.elamur.ai/free/en/papers/zhang-2025-sr-llm-rethinking-structured-representation/)
- [next → Unraveling the Mechanics of Learning-Based Demonstration Selection for In-Context Learning](https://md.research.elamur.ai/free/en/papers/liu-2025-unraveling-mechanics-learning-based-demonstration/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/8/)

## References

55 references, 27 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Alon Albalak, Duy Phung, Nathan Lile, Rafael Rafailov, Kanishk Gandhi, Louis Castricato, Anikait Singh, Chase Blagden, Violet Xiang, Dakota Mahan, and Nick Haber. Big-math: A large-scale, high-quality math dataset for reinforcement learning in language models, 2025. URL https://arxiv.org/abs/2502.1… [↗](https://arxiv.org/abs/2502.1…)
2. Mislav Balunović, Jasper Dekoninck, Ivo Petrov, Nikola Jovanović, and Martin Vechev. [Matharena: Evaluating llms on uncontaminated math competitions](https://md.research.elamur.ai/free/en/papers/balunovic-2025-matharena-evaluating-llms-uncontaminated-math/), February 2025. URL [https://matharena.ai/](https://matharena.ai/) . [↗](https://matharena.ai/)
3. Ralph Allan Bradley and Milton E. Terry. Rank analysis of incomplete block designs: The method of paired comparisons. Biometrika, 39(3-4):324–345, 12 1952. ISSN 0006-3444. doi: 10.1093/ biomet/39.3-4.324. URL https://doi.org/10.1093/biomet/39.3-4.324 . — [doi:10.1093/biomet/39.3-4.324](https://doi.org/10.1093/biomet/39.3-4.324) [↗](https://doi.org/10.1093/biomet/39.3-4.324)
4. 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 Y… [find](https://scholar.google.com/scholar?q=Luoxin+Chen%2C+Jinming+Gu%2C+Liankai+Huang%2C+Wenhao+Huang%2C+Zhicheng+Jiang%2C+Allan+Jie%2C+Xiaoran+Jin%2C+Xing+Jin%2C+Chenggang+Li%2C+Kaijing+Ma%2C+Cheng+Ren%2C+Jiawei+Shen%2C+Wenlei+Shi%2C+Tong+Sun%2C+He+Sun%2C+Jiahui+Wang%2C+Sir)
5. Alexis Chevalier, Jiayi Geng, Alexander Wettig, Howard Chen, Sebastian Mizera, Toni Annala, Max Jameson Aragon, Arturo Rodríguez Fanlo, Simon Frieder, Simon Machado, Akshara Prabhakar, Ellie Thieu, Jiachen T. Wang, Zirui Wang, Xindi Wu, Mengzhou Xia, Wenhan Xia, Jiatong Yu, Junjie Zhu, Zhiyong Jason… — [Language Models as Science Tutors](https://md.research.elamur.ai/free/en/papers/chevalier-2024-language-models-science-tutors/)
6. OpenReview.net, 2024. URL [https://openreview.net/forum?id=](https://openreview.net/forum?id=) WFyolnFZOR . [↗](https://openreview.net/forum?id=)
7. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. [Training verifiers to solve math word problems](https://md.research.elamur.ai/free/en/papers/cobbe-2021-training-verifiers-solve-math-word/). CoRR, abs/2110.14168, 2021. URL https://arxiv.org/abs/2110.1416… [↗](https://arxiv.org/abs/2110.1416…)
8. 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. — [The Lean 4 Theorem Prover and Programming Language (System Description)](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/)
9. Jasper Dekoninck, Maximilian Baader, and Martin T. Vechev. Polyrating: A cost-effective and bias-aware rating system for LLM evaluation. In The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. [find](https://scholar.google.com/scholar?q=Jasper+Dekoninck%2C+Maximilian+Baader%2C+and+Martin+T%2E+Vechev%2E+Polyrating%3A+A+cost%2Deffective+and+bias%2Daware+rating+system+for+LLM+evaluation%2E+In+The+Thirteenth+International+Conference+on+Learning+Represen)
10. OpenReview.net, 2025. URL [https://openreview.net/forum?id=URPwT55i6O](https://openreview.net/forum?id=URPwT55i6O) . [↗](https://openreview.net/forum?id=URPwT55i6O)
11. Simon Frieder, Luca Pinchetti, Alexis Chevalier, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Petersen, and Julius Berner. [Mathematical capabilities of chatgpt](https://md.research.elamur.ai/free/en/papers/frieder-2023-mathematical-capabilities-chatgpt/). In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neu…
12. 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 mathemat… — [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://md.research.elamur.ai/free/en/papers/gao-2024-omni-math-universal-olympiad-level/)
13. OpenReview.net, 2025. URL [https://openreview.net/forum?id=yaqPf0KAlN](https://openreview.net/forum?id=yaqPf0KAlN) . [↗](https://openreview.net/forum?id=yaqPf0KAlN)
14. Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Caroline 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 Bar… — [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://md.research.elamur.ai/free/en/papers/glazer-2024-frontiermath-benchmark-evaluating-advanced-mathematical/)
15. 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, abs/2411.15594, 2024. doi: 10.48550/ARXIV.2411.15594. URL https://doi.org/10. 48550/arXiv.2411.15594 . [find](https://scholar.google.com/scholar?q=Jiawei+Gu%2C+Xuhui+Jiang%2C+Zhichao+Shi%2C+Hexiang+Tan%2C+Xuehao+Zhai%2C+Chengjin+Xu%2C+Wei+Li%2C+Yinghan+Shen%2C+Shengjie+Ma%2C+Honghao+Liu%2C+Yuanzhuo+Wang%2C+and+Jian+Guo%2E+A+survey+on+llm%2Das%2Da%2Djudge%2E+CoRR%2C+abs%2F2411%2E1559)
16. Xinyu Guan, Li Lyna Zhang, Yifei Liu, Ning Shang, Youran Sun, Yi Zhu, Fan Yang, and Mao Yang. [rstar-math: Small llms can master math reasoning with self-evolved deep thinking](https://md.research.elamur.ai/free/en/papers/guan-2025-rstar-math-small-llms-can/). CoRR, abs/2501.04519, 2025. doi: 10.48550/ARXIV.2501.04519. URL https://doi.org/10.48550/ arXiv.2501.04519 .
17. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. [Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning](https://md.research.elamur.ai/free/en/papers/deepseek-ai-2025-deepseek-r1-incentivizing-reasoning-capability/). arXiv preprint arXiv:2501.12948, 2025a.
18. 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 llms for math reasoning, 2025b. URL https://arxiv.org/abs/2506.06877 . — [arXiv:2506.06877](https://arxiv.org/abs/2506.06877) [↗](https://arxiv.org/abs/2506.06877)
19. Chaoqun He, 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](https://md.research.elamur.ai/free/en/papers/he-2024-olympiadbench-challenging-benchmark-promoting-agi/). In Lun-We…
20. 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 verifiable mathematical dataset for advancing reason… — [DeepMath-103K: A Large-Scale, Challenging, Decontaminated, and Verifiable Mathematical Dataset for Advancing Reasoning](https://md.research.elamur.ai/free/en/papers/he-2025-deepmath-103k-large-scale-challenging/)
21. Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-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, An… — [OpenAI o1 System Card](https://md.research.elamur.ai/free/en/papers/openai-2024-openai-o1-system-card/)
22. 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. [https://huggingface.co/AI-MO/NuminaMath-1.5](https://github.co… [find](https://scholar.google.com/scholar?q=Jia+Li%2C+Edward+Beeching%2C+Lewis+Tunstall%2C+Ben+Lipkin%2C+Roman+Soletskyi%2C+Shengyi+Costa+Huang%2C+Kashif+Rasul%2C+Longhui+Yu%2C+Albert+Jiang%2C+Ziju+Shen%2C+Zihan+Qin%2C+Bin+Dong%2C+Li+Zhou%2C+Yann+Fleureau%2C+Guillaume+Lam)
23. Hunter Lightman, Vineet 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](https://md.research.elamur.ai/free/en/papers/lightman-2023-let-s-verify-step-step/).
24. OpenReview.net, 2024. URL [https://openreview.net/forum?id=v8L0pN6EOi](https://openreview.net/forum?id=v8L0pN6EOi) . [↗](https://openreview.net/forum?id=v8L0pN6EOi)
25. 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: A frontier model for open-source automated theorem proving](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/). CoRR, abs/2502.07640, 2025a. doi: 10.48550/ARXIV.2502.07640. URL https://doi.org/10.48550/ar… [↗](https://doi.org/10.48550/ar…)
26. 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 sc… — [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-v2-scaling-formal/)
27. Yantao Liu, Zijun Yao, Rui Min, Yixin Cao, Lei Hou, and Juanzi Li. Pairjudge rm: Perform best-of-n sampling with knockout tournament, 2025. URL https://arxiv.org/abs/2501.13007 . — [arXiv:2501.13007](https://arxiv.org/abs/2501.13007) [↗](https://arxiv.org/abs/2501.13007)
28. 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.48550/ARXIV.2504.01995. URL https://d… [find](https://scholar.google.com/scholar?q=Hamed+Mahdavi%2C+Alireza+Hashemi%2C+Majid+Daliri%2C+Pegah+Mohammadipour%2C+Alireza+Farhadi%2C+Samira+Malek%2C+Yekta+Yazdanifard%2C+Amir+Khasahmadi%2C+and+Vasant+G%2E+Honavar%2E+Brains+vs%2E+bytes%3A+Evaluating+LLM+proficienc)
29. Philipp Mondorf and Barbara Plank. Beyond accuracy: Evaluating the reasoning behavior of large language models - A survey. CoRR, abs/2404.[01869, 2024](https://md.research.elamur.ai/free/en/papers/mondorf-2024-accuracy-evaluating-reasoning-behavior-large/). doi: 10.48550/ARXIV.2404.01869. URL https://doi.org/10.48550/arXiv.2404.01869 . [↗](https://doi.org/10.48550/arXiv.2404.01869)
30. Ivan Moshkov, Darragh Hanley, Ivan Sorokin, Shubham Toshniwal, Christof Henkel, Benedikt Schifferer, Wei Du, and Igor Gitman. AIMO-2 winning solution: Building state-of-the-art mathematical reasoning models with openmathreasoning dataset. CoRR, abs/2504.16891, 2025. doi: 10.48550/ARXIV.2504.16891. U… [find](https://scholar.google.com/scholar?q=Ivan+Moshkov%2C+Darragh+Hanley%2C+Ivan+Sorokin%2C+Shubham+Toshniwal%2C+Christof+Henkel%2C+Benedikt+Schifferer%2C+Wei+Du%2C+and+Igor+Gitman%2E+AIMO%2D2+winning+solution%3A+Building+state%2Dof%2Dthe%2Dart+mathematical+reasoning+)
31. Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002. [find](https://scholar.google.com/scholar?q=Tobias+Nipkow%2C+Lawrence+C+Paulson%2C+and+Markus+Wenzel%2E+Isabelle%2FHOL%3A+a+proof+assistant+for+higher%2Dorder+logic%2C+volume+2283%2E+Springer+Science+%26+Business+Media%2C+2002%2E)
32. OpenAI. Openai o3 and o4-mini system card, April 2025. URL [https://cdn.openai.com/pdf/](https://cdn.openai.com/pdf/) 2221c875-02dc-4789-800b-e7758f3722c1/o3-and-o4-mini-system-card.pdf . [↗](https://cdn.openai.com/pdf/)
33. 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 Paquet, Jakub M. Tomczak, and Cheng Zhang, editors, Advances in Neural Information Processing Systems 38: Annual Confe… [find](https://scholar.google.com/scholar?q=Arjun+Panickssery%2C+Samuel+R%2E+Bowman%2C+and+Shi+Feng%2E+LLM+evaluators+recognize+and+favor+their+own+generations%2E+In+Amir+Globersons%2C+Lester+Mackey%2C+Danielle+Belgrave%2C+Angela+Fan%2C+Ulrich+Paquet%2C+Jakub+M%2E+T)
34. Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunovic, Nikola Jovanovic, and Martin T. Vechev. Proof or bluff? evaluating llms on 2025 USA math olympiad. CoRR, abs/2503.21934, 2025. doi: 10.48550/ARXIV.2503.21934. URL https://doi.org/10.48550/arXiv.250… [↗](https://doi.org/10.48550/arXiv.250…)
35. Qwen Team. Qwen3: Think Deeper, Act Faster, April 2025. URL [https://qwenlm.github.io/](https://qwenlm.github.io/) blog/qwen3/ . Qwen Blog. [↗](https://qwenlm.github.io/)
36. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcemen… — [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/)
37. 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](https://md.research.elamur.ai/free/en/papers/shao-2024-deepseekmath-pushing-limits-mathematical-reasoning/). CoRR, abs/2402.03300, 2024. doi: 10.48550/ARXIV.2402.03300. URL https://doi.org/10.48550/arXiv.2402.03300… [↗](https://doi.org/10.48550/arXiv.2402.03300…)
38. 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](https://md.research.elamur.ai/free/en/papers/sheng-2024-hybridflow-flexible-efficient-rlhf-framework/). arXiv preprint arXiv: 2409.19256, 2024.
39. Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, and Pan Lu. Solving inequality proofs with large language models, 2025. URL https://arxiv.org/abs/2506.07927 . — [arXiv:2506.07927](https://arxiv.org/abs/2506.07927) [↗](https://arxiv.org/abs/2506.07927)
40. Parshin Shojaee, 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](https://md.research.elamur.ai/free/en/papers/shojaee-2025-illusion-thinking-understanding-strengths-limitations/), 2025. URL https://arxiv.org/abs/2506.06941 . [↗](https://arxiv.org/abs/2506.06941)
41. Gemini Team. [Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities](https://md.research.elamur.ai/free/en/papers/comanici-2025-gemini-2-5-pushing-frontier/). CoRR, abs/2507.06261, 2025. doi: 10.48550/ ARXIV.2507.06261. URL https://doi.org/10.48550/arXiv.2507.06261 . [↗](https://doi.org/10.48550/arXiv.2507.06261)
42. 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](https://md.research.elamur.ai/free/en/papers/tsoukalas-2024-putnambench-evaluating-neural-theorem-provers/). In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jak…
43. 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, Lo… — [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/)
44. Shijie Xia, Xuefeng Li, Yixin Liu, Tongshuang Wu, and Pengfei Liu. [Evaluating mathematical reasoning beyond accuracy](https://md.research.elamur.ai/free/en/papers/xia-2024-evaluating-mathematical-reasoning-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,…
45. AAAI Press, 2025. doi: 10.1609/AAAI.V39I26.34987. URL https://doi.org/10.1609/aaai.v39i26.34987 . — [doi:10.1609/aaai.v39i26.34987](https://doi.org/10.1609/aaai.v39i26.34987) [↗](https://doi.org/10.1609/aaai.v39i26.34987)
46. 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. Formalmath: Benchmarking formal mathematical reasoning of large language models, 2025. URL https://arxiv.org/abs/2505.02735 . [↗](https://arxiv.org/abs/2505.02735)
47. 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 Kaplan, Michele Lunati, and Summer Yue. [A careful examination of large language model performance on grade school arithmetic](https://md.research.elamur.ai/free/en/papers/zhang-2024-careful-examination-large-language-model/). In Amir G…
48. 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: Advancing llm reasoning for theorem proving through natural language and reinforcement learning, 2025. URL [https://arxiv.org/…](https://arxiv.org/…) — [arXiv:2505.23754](https://arxiv.org/abs/2505.23754) [↗](https://arxiv.org/…)
49. Chenyan Zhao, Mariana Silva, and Seth Poulsen. Autograding mathematical induction proofs with natural language processing. CoRR, abs/2406.10268, 2024. doi: 10.48550/ARXIV.2406.10268. URL https://doi.org/10.48550/arXiv.2406.10268 . — [doi:10.48550/arxiv.2406.10268](https://doi.org/10.48550/arxiv.2406.10268) [↗](https://doi.org/10.48550/arXiv.2406.10268)
50. 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… [find](https://scholar.google.com/scholar?q=Chenyan+Zhao%2C+Mariana+Silva%2C+and+Seth+Poulsen%2E+Language+models+are+few%2Dshot+graders%2E+In+Alexandra+I%2E+Cristea%2C+Erin+Walker%2C+Yu+Lu%2C+Olga+C%2E+Santos%2C+and+Seiji+Isotani%2C+editors%2C+Artificial+Intelligence+in)
51. Springer, 2025. doi: 10.1007/978-3-031-98459-4\\_1. URL https://doi.org/10.1007/ 978-3-031-98459-4_1 . — [doi:10.1007/978-3-031-98459-4\\_1](https://doi.org/10.1007/978-3-031-98459-4_1) [find](https://scholar.google.com/scholar?q=Springer%2C+2025%2E+doi%3A+10%2E1007%2F978%2D3%2D031%2D98459%2D4%5C%5C%5F1%2E+URL+https%3A%2F%2Fdoi%2Eorg%2F10%2E1007%2F+978%2D3%2D031%2D98459%2D4%5F1+%2E+%E2%80%94+%5Bdoi%3A10%2E1007%2F978%2D3%2D031%2D98459%2D4%5C%5C%5F1%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1007%2F978%2D3%2D031%2D98459%2D4%5F1%29)
52. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [minif2f: a cross-system benchmark for formal olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022.
53. OpenReview.net, 2022. URL [https://openreview.net/forum?id=9ZPegFuFTFv](https://openreview.net/forum?id=9ZPegFuFTFv) . [↗](https://openreview.net/forum?id=9ZPegFuFTFv)
54. Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. [Judging llm-as-a-judge with mt-bench and chatbot arena](https://md.research.elamur.ai/free/en/papers/zheng-2023-judging-llm-judge-mt-bench/). In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Morit…
55. HS HS HS HS HS HS UG HS HS HS UG HS HS HS HS I I N N N I I I I N I I N N N 31.7% 68.1% 78.3% 87.5% 63.5% 37.8% 62.2% 18.0% 34.2% 92.0% 100.0% 43.3% 87.5% 52.2% 35.1% Public Public Public Public Public Public Public Public Public Public Public Private Public Public Public UG [find](https://scholar.google.com/scholar?q=HS+HS+HS+HS+HS+HS+UG+HS+HS+HS+UG+HS+HS+HS+HS+I+I+N+N+N+I+I+I+I+N+I+I+N+N+N+31%2E7%25+68%2E1%25+78%2E3%25+87%2E5%25+63%2E5%25+37%2E8%25+62%2E2%25+18%2E0%25+34%2E2%25+92%2E0%25+100%2E0%25+43%2E3%25+87%2E5%25+52%2E2%25+35%2E1%25+Public+Public+Public+Public+Public)

*Updated 2 November 2026*