Fetching the paper…
Reading the bibliography…
A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data.
Isabelle/HOL: a proof assistant for higher-order logic
Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson · 2002
Earlier work this paper cites.
Automated theorem proving
Wolfgang Bibel · 2013
Earlier work this paper cites.
Adam: A method for stochastic optimization
Diederik P Kingma and Jimmy Ba · 2014
Earlier work this paper cites.
Automated theorem proving: A logical basis
Donald W Loveland · 2016
Earlier work this paper cites.
Mastering the game of Go with deep neural networks and tree search
David Silver, Aja Huang, Christopher J. Maddison, Arthur Guez, Laurent Sifre, George van den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy Lillicrap, Madeleine Leach, Koray Kavukcuoglu, Thore Graepel, and Demis Hassabis · 2016
Earlier work this paper cites.
Hindsight experience replay
Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, OpenAI Pieter Abbeel, and Wojciech Zaremba · 2017
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.
Reinforcement learning of theorem proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák · 2018
Earlier work this paper cites.
Dual policy iteration
Wen Sun, Geoffrey J Gordon, Byron Boots, and J Bagnell · 2018
Earlier work this paper cites.
The lean mathematical library
The mathlib Community · 2020
Earlier work this paper cites.
Automatic curriculum learning for deep rl: A short survey
Rémy Portelas, Cédric Colas, Lilian Weng, Katja Hofmann, and Pierre-Yves Oudeyer · 2020
Earlier work this paper cites.
First neural conjecturing datasets and experiments
Josef Urban and Jan Jakubův · 2020
Earlier work this paper cites.
Learning to prove theorems by learning to generate theorems
Mingzhe Wang and Jia Deng · 2020
Earlier work this paper cites.
Int: An inequality benchmark for evaluating generalization in theorem proving
Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, and Roger Grosse · 2020
Earlier work this paper cites.
Lisa: Language models of isabelle proofs
Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu · 2021
Earlier work this paper cites.
The lean 4 theorem prover and programming language
Leonardo de Moura and Sebastian Ullrich · 2021
Earlier work this paper cites.
Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning
Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli · 2021
Earlier work this paper cites.
minif2f: a cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2021
Earlier work this paper cites.
Proving theorems using incremental learning and hindsight experience replay
Eser Aygün, Ankit Anand, Laurent Orseau, Xavier Glorot, Stephen M Mcaleer, Vlad Firoiu, Lei M Zhang, Doina Precup, and Shibl Mourad · 2022
Cited alongside, same era.
Autotelic agents with intrinsically motivated goal-conditioned reinforcement learning: a short survey
Cédric Colas, Tristan Karch, Olivier Sigaud, and Pierre-Yves Oudeyer · 2022
Cited alongside, same era.
Language models can teach themselves to program better
Patrick Haluptzok, Matthew Bowers, and Adam Tauman Kalai · 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
Cited alongside, same era.
Codegen: An open large language model for code with multi-turn program synthesis
Erik Nijkamp, Bo Pang, Hiroaki Hayashi, Lifu Tu, Huan Wang, Yingbo Zhou, Silvio Savarese, and Caiming Xiong · 2022
Ai achieves silver-medal standard solving international mathematical olympiad problems
AlphaProof · 2024
Later among the works it cites.
Formal theorem proving by rewarding llms to decompose proofs hierarchically
Kefan Dong, Arvind Mahankali, and Tengyu Ma · 2024
Later among the works it cites.
On lemma conjecturing using neural, symbolic and neuro-symbolic approaches
Sólrún Halla Einarsdóttir, Yousef Alhessi, Emily First, and Moa Johansson · 2024
Later among the works it cites.
Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, et al · 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
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Evolving curricula with regret-based environment design
Jack Parker-Holder, Minqi Jiang, Michael Dennis, Mikayel Samvelyan, Jakob Foerster, Edward Grefenstette, and Tim Rocktäschel · 2022
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.
React: Synergizing reasoning and acting in language models
Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao · 2022
Cited alongside, same era.
Multilingual mathematical autoformalization
Albert Q Jiang, Wenda Li, and Mateja Jamnik · 2023
Cited alongside, same era.
Exploring mathematical conjecturing with large language models
Moa Johansson and Nicholas Smallbone · 2023
Cited alongside, same era.
Efficient memory management for large language model serving with pagedattention
Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph Gonzalez, Hao Zhang, and Ion Stoica · 2023
Cited alongside, same era.
Starcoder: may the source be with you!
Raymond Li, Loubna Ben Allal, Yangtian Zi, Niklas Muennighoff, Denis Kocetkov, Chenghao Mou, Marc Marone, Christopher Akiki, Jia Li, Jenny Chim, et al · 2023
Cited alongside, same era.
Later among the works it cites.
Process-driven autoformalization in lean 4
Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al · 2024
Later among the works it cites.
Reasoning with large language models, a survey
Aske Plaat, Annie Wong, Suzan Verberne, Joost Broekens, Niki van Stein, and Thomas Back · 2024
Later among the works it cites.
Learning formal mathematics from intrinsic motivation
Gabriel Poesia, David Broman, Nick Haber, and Noah D Goodman · 2024
Later among the works it cites.
Autotelic llm-based exploration for goal-conditioned rl
Guillaume Pourcel, Thomas Carta, Grgur Kovač, and Pierre-Yves Oudeyer · 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, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo · 2024
Later among the works it cites.
Alphageometry: An olympiad-level ai system for geometry
Trieu Trinh and Thang Luong · 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.
Evolving alignment via asymmetric self-play
Ziyu Ye, Rishabh Agarwal, Tianqi Liu, Rishabh Joshi, Sarmishta Velury, Quoc V Le, Qijun Tan, and Yuan Liu · 2024
Later among the works it cites.
Lean workbook: A large-scale lean problem set formalized from natural language math problems
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen · 2024
Later among the works it cites.
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.