Holophrasm: a neural Automated Theorem Prover for higher-order logic. arXiv preprint 2016 [pdf]
Daniel Whalen
Deep Network Guided Proof Search. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning 2017 [pdf]
Sarah Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk
Reinforcement Learning of Theorem Proving. NeurIPS 2018 [pdf]
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olšák
GamePad: A Learning Environment for Theorem Proving. ICLR 2019 [pdf] [code]
Daniel Huang, Prafulla Dhariwal, Dawn Song, Ilya Sutskever
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. ICML 2019 [pdf] [dataset]
Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, Stewart Wilcox
Learning to Prove Theorems via Interacting with Proof Assistants. ICML 2019 [pdf] [code]
Kaiyu Yang, Jia Deng
Graph Representations for Higher-Order Logic and Theorem Proving. AAAI 2020 [pdf]
Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, Christian Szegedy
Generative Language Modeling for Automated Theorem Proving. arXiv preprint 2020 [pdf]
Stanislas Polu, Ilya Sutskever
Learning to Prove Theorems by Learning to Generate Theorems. NeurIPS 2020 [pdf] [code]
Mingzhe Wang, Jia Deng
TacticToe: Learning to Prove with Tactics. Journal of Automated Reasoning 2021 [pdf]
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving. AAAI 2021 [pdf] [code]
Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, Achille Fokoue
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. NeurIPS 2021 [pdf]
Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli
Learning to Guide a Saturation-Based Theorem Prover. TPAMI 2022 [pdf] [code]
Ibrahim Abdelaziz, Maxwell Crouse, Bassem Makni, Vernon Austil, Cristina Cornelio, Shajith Ikbal, Pavan Kapanipathi, Ndivhuwo Makondo, Kavitha Srinivas, Michael Witbrock, Achille Fokoue
Proof Artifact Co-training for Theorem Proving with Language Model. ICLR 2022 [pdf] [tactic step data] [PACT data]
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu
Formal Mathematics Statement Curriculum Learning. ICML 2022 [pdf]
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, Ilya Sutskever
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. NeurIPS 2022 [pdf]
Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, Mateja Jamnik
NaturalProver: Grounded Mathematical Proof Generation with Language Models. NeurIPS 2022 [pdf] [code]
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, Yejin Choi
HyperTree Proof Search for Neural Theorem Proving. NeurIPS 2022 [pdf]
Guillaume Lample, Timothee Lacroix, Marie-anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, Xavier Martinet
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. ICLR 2023 [pdf] [code]
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, Yuhuai Wu
Baldur: Whole-Proof Generation and Repair with Large Language Models arxiv preprint 2023 [pdf]
Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun
Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving. arXiv preprint 2023 [pdf] [code]
Xueliang Zhao, Wenda Li, Lingpeng Kong
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. NeurIPS 2023 Datasets and Benchmarks Track [pdf] [code]
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar
DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. ACL 2023 [pdf]
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, Xiaodan Liang
Lyra: Orchestrating Dual Correction in Automated Theorem Proving. arXiv preprint 2023 [pdf] [code]
Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, Yu Li
A Language-Agent Approach to Formal Theorem-Proving. arXiv preprint 2023 [pdf]
Amitayush Thakur, Yeming Wen, Swarat Chaudhuri
LEGO-Prover: Neural Theorem Proving with Growing Libraries. ICLR 2024 [pdf] [code]
Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, Xiaodan Liang
LLMSTEP: LLM proofstep suggestions in Lean. The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS 2023 [pdf] [code]
Sean Welleck, Rahul Saha
Temperature-scaled large language models for Lean proofstep prediction. The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS 2023 [pdf]
Fabian Gloeckle, Baptiste Roziere, Amaury Hayat, Gabriel Synnaeve
Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving. arXiv preprint 2024 [pdf] [code]
Jason Rute, Miroslav Olšák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun
Solving olympiad geometry without human demonstrations. Nature 2024 [pdf][code]
Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, Thang Luong
FGeo-TP: A Language Model-Enhanced Solver for Geometry Problems. Symmetry 2024 [pdf]
Yiming He, Jia Zou, Xiaokai Zhang, Na Zhu, Tuo Leng
FGeo-HyperGNet: Geometry Problem Solving Integrating Formal Symbolic System and Hypergraph Neural Network. arXiv preprint 2024 [pdf][code]
Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Cheng Qin, Yang Li, Zhenbing Zeng, Tuo Leng
FGeo-SSS: A Search-Based Symbolic Solver for Human-like Automated Geometric Reasoning. Symmetry 2024 [pdf]
Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Cheng Qin, Yang Li, Tuo Leng
FGeo-DRL: Deductive Reasoning for Geometric Problems through Deep Reinforcement Learning. Symmetry 2024 [pdf]
Jia Zou, Xiaokai Zhang, Yiming He, Na Zhu, Tuo Leng
Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry. arXiv preprint 2024 [pdf][code]
Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat, Matthias Bethge
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving. ACL 2024 [pdf] [dataset]
Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang
Proving Theorems Recursively. arXiv preprint 2024 [pdf] [code]
Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, Xiaodan Liang
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data. arXiv preprint 2024 [pdf]
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, Xiaodan Liang
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. arXiv preprint 2024 [pdf] [code]
Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, Chong Ruan
Learning to Prove Theorems by Learning to Generate Theorems. NeurIPS 2020 [pdf] [code]
Mingzhe Wang, Jia Deng
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. ICLR 2021 [pdf] [code]
Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, Roger Grosse
Solving olympiad geometry without human demonstrations. Nature 2024 [pdf][code]
Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, Thang Luong
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data. ICLR 2024 [pdf][code]
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, Xiaodan Liang
ATG: Benchmarking Automated Theorem Generation for Generative Language Models. NAACL 2024 [pdf]
Xiaohan Lin, Qingxing Cao, Yinya Huang, Zhicheng Yang, Zhengying Liu, Zhenguo Li, Xiaodan Liang
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. CPP 2020 [pdf]
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, Josef Urban
Autoformalization with Large Language Models. NeurIPS 2022 [pdf]
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, Christian Szegedy
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics. arXiv preprint 2023 [pdf] [code]
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad
Multilingual Mathematical Autoformalization. arXiv preprint 2023 [pdf] [code]
Albert Q. Jiang, Wenda Li, Mateja Jamnik
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems. arXiv preprint 2024 [pdf] [dataset] [code]
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, Kai Chen
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts. EMNLP 2024 [pdf] [code]
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang
REFACTOR: Learning to Extract Theorems from Proofs. ICLR 2024 [pdf] [code]
Jin Peng Zhou, Yuhuai Wu, Qiyang Li, Roger Grosse
DeepMath - Deep Sequence Models for Premise Selection. NeurIPS 2016 [pdf]
Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban
Premise Selection for Theorem Proving by Deep Graph Embedding. NeurIPS 2017 [pdf]
Mingzhe Wang, Yihe Tang, Jian Wang, Jia Deng
Natural Language Premise Selection: Finding Supporting Statements for Mathematical Text. LREC 2020 [pdf] [code]
Deborah Ferreira, André Freitas
Premise Selection in Natural Language Mathematical Texts. ACL 2020 [pdf]
Deborah Ferreira, André Freitas
Machine-Learned Premise Selection for Lean arXiv preprint 2023 [pdf] [code]
Bartosz Piotrowski, Ramon Fernández Mir, Edward Ayers
Magnushammer: A Transformer-based Approach to Premise Selection. ICLR 2024 [pdf]
Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, Yuhuai Wu
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. ICLR 2017 [pdf] [dataset] [code]
Cezary Kaliszyk, François Chollet, Christian Szegedy
Learning to Prove Theorems via Interacting with Proof Assistants. ICML 2019 [pdf] [code]
Kaiyu Yang, Jia Deng
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. ICML 2019 [pdf] [dataset]
Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, Stewart Wilcox
IsarStep: a Benchmark for High-level Mathematical Reasoning. ICLR 2021 [pdf] [code]
Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. ICLR 2021 [pdf] [code]
Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, Roger Grosse
NaturalProofs: Mathematical Theorem Proving in Natural Language. NeurIPS 2021 Datasets and Benchmarks Track (Round 1) [pdf] [code]
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, Kyunghyun Cho
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. ICLR 2022 [pdf] [dataset]
Kunhao Zheng, Jesse Michael Han, Stanislas Polu
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics. arXiv preprint 2023 [pdf] [code]
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad
Evaluating Language Models for Mathematics through Interactions. arXiv preprint 2023 [pdf] [code]
Katherine M. Collins, Albert Q. Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B. Tenenbaum, William Hart, Timothy Gowers, Wenda Li, Adrian Weller, Mateja Jamnik
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. NeurIPS 2023 Datasets and Benchmarks Track [pdf] [code]
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar
FIMO: A Challenge Formal Dataset for Automated Theorem Proving. arXiv preprint 2023 [pdf]
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, Qun Liu
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models. EMNLP 2023 [pdf] [code]
Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, Qun Liu
MLFMF: Data Sets for Machine Learning for Mathematical Formalization. NeurIPS 2023 [pdf] [code]
Andrej Bauer, Matej Petković, Ljupčo Todorovski
FormalGeo: The First Step Toward Human-like IMO-level Geometric Automated Reasoning. arXiv preprint 2023 [pdf] [code]
Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang, Xiaoxiao Jin, Yanjun Guo, Chenyang Mao, Zhe Zhu, Dengfeng Yue, Fangzhen Zhu, Yang Li, Yifan Wang, Yiwen Huang, Runan Wang, Cheng Qin, Zhenbing Zeng, Shaorong Xie, Xiangfeng Luo, Tuo Leng
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data. ICLR 2024 [pdf][code]
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, Xiaodan Liang
ATG: Benchmarking Automated Theorem Generation for Generative Language Models. NAACL 2024 [pdf]
Xiaohan Lin, Qingxing Cao, Yinya Huang, Zhicheng Yang, Zhengying Liu, Zhenguo Li, Xiaodan Liang
Advancing mathematics by guiding human intuition with AI. Nature 2021 [pdf]
Alex Davies, Petar Veličković, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomašev, Richard Tanburn, Peter Battaglia, Charles Blundell, András Juhász, Marc Lackenby, Geordie Williamson, Demis Hassabis & Pushmeet Kohli
Machine Learning Kreuzer--Skarke Calabi--Yau Threefolds. arXiv preprint 2021 [pdf]
Per Berglund, Ben Campbell, Vishnu Jejjala
Machine Learning Calabi-Yau Hypersurfaces. Physical Review D 2022 [pdf]
David S. Berman, Yang-Hui He, Edward Hirst
Machine learning assisted exploration for affine Deligne-Lusztig varieties. Peking Mathematical Journal 2024 [pdf] [code]
Bin Dong, Xuhua He, Pengfei Jin, Felix Schremmer, Qingchao Yu
Can Transformers Do Enumerative Geometry? arXiv preprint 2024 [pdf]
Baran Hashemi, Roderic G. Corominas, Alessandro Giacchetto
Constructions in combinatorics via neural networks. arXiv preprint 2021 [pdf]
Adam Zsolt Wagner
Searching for ribbons with machine learning. arXiv preprint 2023 [pdf]
Sergei Gukov, James Halverson, Ciprian Manolescu, Fabian Ruehle
Mathematical discoveries from program search with large language models. Nature 2024 [pdf][code]
Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, Alhussein Fawzi