Fetching the paper…
Reading the bibliography…
We introduce Goedel-Prover, an open-source language model that achieves state-of-the-art (as of April 5 2025) performance in automated formal proof generation for mathematical problems.
Isabelle: A generic theorem prover
Lawrence C Paulson · 1994
Earlier work this paper cites.
The Coq proof assistant reference manual: Version 6.1
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al · 1997
Earlier work this paper cites.
Handbook of automated reasoning , volume 1
Alan JA Robinson and Andrei Voronkov · 2001
Earlier work this paper cites.
Z3: An efficient smt solver
Leonardo De Moura and Nikolaj Bjørner · 2008
Earlier work this paper cites.
MaLeCoP machine learning connection prover
Josef Urban, Jiří Vyskočil, and Petr Štěpánek · 2011
Earlier work this paper cites.
First-order theorem proving and vampire
Laura Kovács and Andrei Voronkov · 2013
Earlier work this paper cites.
The lean theorem prover (system description)
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer · 2015
Earlier work this paper cites.
Deepmath-deep sequence models for premise selection
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban · 2016
Earlier work this paper cites.
Thinking fast and slow with deep learning and tree search
Thomas Anthony, Zheng Tian, and David Barber · 2017
Earlier work this paper cites.
Sympy: symbolic computing in python
Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ondřej Čertík, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al · 2017
Earlier work this paper cites.
Reinforcement learning of theorem proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák · 2018
Earlier work this paper cites.
Faster, higher, stronger: E 2.3
Stephan Schulz, Simon Cruanes, and Petar Vukmirović · 2019
Earlier work this paper cites.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2020
Earlier work this paper cites.
Training verifiers to solve math word problems
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al · 2021
Earlier work this paper cites.
Measuring mathematical problem solving with the math dataset
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt · 2021
Earlier work this paper cites.
The Lean 4 theorem prover and programming language
Leonardo de Moura and Sebastian Ullrich · 2021
Cited alongside, same era.
Minif2f: a cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2021
Cited alongside, same era.
cvc5: A versatile and industrial-strength smt solver
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al · 2022
Cited alongside, same era.
Draft, sketch, and prove: Guiding formal theorem provers with informal proofs
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample · 2022
Cited alongside, same era.
Hypertree proof search for neural theorem proving
Guillaume Lample, Timothee Lacroix, Marie anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet · 2022
Odin: Disentangled reward mitigates hacking in rlhf
Lichang Chen, Chen Zhu, Davit Soselia, Jiuhai Chen, Tianyi Zhou, Tom Goldstein, Heng Huang, Mohammad Shoeybi, and Bryan Catanzaro · 2024
Later among the works it cites.
AI achieves silver-medal standard solving international mathematical olympiad problems
Google DeepMind · 2024
Later among the works it cites.
Lean-STaR: Learning to interleave thinking and proving
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck · 2024
Later among the works it cites.
Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, et al · 2024
Later among the works it cites.
American invitational mathematics examination - aime
MAA · 2024
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Formal mathematics statement curriculum learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2022
Cited alongside, same era.
Natural language processing with transformers
Lewis Tunstall, Leandro Von Werra, and Thomas Wolf · 2022
Cited alongside, same era.
Autoformalization with large language models
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy · 2022
Cited alongside, same era.
Proofnet: Autoformalizing and formally proving undergraduate-level mathematics
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad · 2023
Cited alongside, same era.
Baldur: Whole-proof generation and repair with large language models
Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun · 2023
Cited alongside, same era.
Formal mathematics statement curriculum learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2023
Cited alongside, same era.
Direct preference optimization: Your language model is secretly a reward model
Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn · 2023
Cited alongside, same era.
Later among the works it cites.
Magnushammer: A transformer-based approach to premise selection
Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu · 2024
Later among the works it cites.
Orca-math: Unlocking the potential of slms in grade school math
Arindam Mitra, Hamed Khanpour, Corby Rosset, and Ahmed Awadallah · 2024
Later among the works it cites.
Deepseekmath: Pushing the limits of mathematical reasoning in open language models
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al · 2024
Later among the works it cites.
Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri · 2024
Later among the works it cites.
Theoremllama: Transforming general-purpose llms into lean4 experts
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang · 2024
Later among the works it cites.
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen · 2024
Later among the works it cites.
https://artofproblemsolving.com/wiki/
Art of problem solving wiki · 2025
Closest in time.
Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning
Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al · 2025
Closest in time.
mathlib4: The math library of lean 4, 2023
mathlib4 · 2025
Closest in time.