We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.
Czech Technical University in Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）；Institut des Hautes Études Scientifiques（高等科学研究所）；Radboud University（拉德堡德大学）
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
School of Mathematical Sciences, Peking University（北京大学数学科学学院）；IQuest Research（IQuest研究院）；Research Institute for Mathematical Sciences, Kyoto University（京都大学数学研究所）；Westlake Institute for Advanced Study, Westlake University（西湖研究所在线高级研究院）；Beijing International Center for Mathematical Research and the New Cornerstone Science Laboratory, Peking University（北京国际数学研究中心和新基石科学实验室，北京大学）；Center for Machine Learning Research, Peking University（北京大学机器学习研究中心）；Center for Intelligent Computing, Great Bay Institute for Advanced Study, Great Bay University（智能计算中心，Great Bay高级研究院，Great Bay大学）；Zhongguancun Academy（中关村学院）
Combining Textual and Structural Information for Premise Selection in Lean
Faculty of Mathematics and Physics, University of Ljubljana（卢布尔雅纳大学数学与物理学院）；University of Ljubljana（卢布尔雅纳大学）；Department of Knowledge Technologies, Jožef Stefan Institute（知识技术系，乔泽夫·斯塔芬研究所）
Magnushammer: A Transformer-Based Approach to Premise Selection
Google Research（谷歌研究院）；Google DeepMind（谷歌DeepMind）；University of Warsaw（华沙大学）；xAI（xAI公司）；Mistral AI（Mistral AI公司）；IDEAS NCBR；University of Cambridge（剑桥大学）；Cornell University（康奈尔大学）
Stateful Premise Selection by Recurrent Neural Networks
Czech Institute of Informatics, Robotics and Cybernetics（捷克信息学、机器人与控制论研究所）；Faculty of Mathematics, Informatics and Mechanics, University of Warsaw（华沙大学数学、信息学与力学学院）
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
Czech Institute of Informatics, Robotics and Cybernetics（捷克信息学、机器人学与控制论研究所）；Faculty of Mathematics, Informatics and Mechanics, University of Warsaw（华沙大学数学、信息学与力学学院）
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
University of Cambridge（剑桥大学）；University of Warsaw（华沙大学）；IDEAS NCBR（IDEAS国家生物医学研究中心）；Polish Academy of Sciences（波兰科学院）；Google Research（谷歌研究院）；Stanford University（斯坦福大学）
Czech Technical University in Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）；INDRC；Institut des Hautes Études Scientifiques（高等科学研究所）；DHBW Stuttgart（斯图加特双元制大学）
Learning Guided Automated Reasoning: A Brief Survey
Czech Technical University in Prague（捷克技术大学布拉格）；Radboud University Nijmegen（拉德堡德大学奈杰姆）；Czech Academy of Sciences Institute for Computer Science（捷克科学院计算机科学研究所）；University of Innsbruck（因斯布鲁克大学）
