AI for Mathematics (AI4Math) Papers

Table of Contents

• Automated Theorem Proving
• Synthetic Theorem Generation
• Autoformalization
• Proof Refactoring
• Premise Selection
• Benchmarks
• Human-in-the-loop
• Constructing Examples / Counterexamples

Automated Theorem Proving

• 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

Synthetic Theorem Generation

• 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

Autoformalization

• 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

Proof Refactoring

• REFACTOR: Learning to Extract Theorems from Proofs. ICLR 2024 [pdf] [code]

  Jin Peng Zhou, Yuhuai Wu, Qiyang Li, Roger Grosse

Premise Selection

• 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

Benchmarks

• 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

Human-in-the-loop

• 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

Constructing Examples / Counterexamples

• 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