Title
Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving Chuxue Cao Mengze Li Juntao Dai Jinluan Yang Zijian Zhao Shengyu Zhang Weijie Shi Chengzhong Liu Sirui Han Yike Guo LRM 26 0 0 20 Jun 2025
LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs Manooshree Patel Rayna Bhattacharyya Thomas Lu Arnav Mehta Niels Voss Narges Norouzi Gireeja Ranade 56 0 0 10 Jun 2025
Premise Selection for a Lean Hammer Thomas Zhu Joshua Clune Jeremy Avigad Albert Qiaochu Jiang Sean Welleck 31 0 0 09 Jun 2025
Mathesis: Towards Formal Theorem Proving from Natural Languages Yu Xuejun Jianyuan Zhong Zijin Feng Pengyi Zhai Roozbeh Yousefzadeh ... Dongcai Lu Jiacheng Sun Q. Xu Shen Xin Zhenguo Li AIMat OffRL LRM 27 0 0 08 Jun 2025
Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine Zhuoxuan Jiang T. Zhang Peiyan Peng Jing Chen Yinong Xun Haotian Zhang L. Li Yong Li Shaohua Zhang AI4CE 57 0 0 03 Jun 2025
Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks Debargha Ganguly Vikash Singh Sreehari Sankar Biyao Zhang Xuecen Zhang Srinivasan Iyengar Xiaotian Han Amit Sharma Shivkumar Kalyanaraman Vipin Chaudhary 76 0 0 26 May 2025
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement Jilin Hu Jianyu Zhang Yongwang Zhao Talia Ringer 52 1 0 21 May 2025
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation Junyu Lai Jiakun Zhang Shuo Xu Taolue Chen Zihang Wang Yao Yang Jiarui Zhang Chun Cao Jingwei Xu 115 0 0 17 May 2025
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation Zhenwen Liang Linfeng Song Yang Li Tao Yang Feng Zhang Haitao Mi Dong Yu LRM 150 2 0 16 May 2025
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning Azim Ospanov Farzan Farnia Roozbeh Yousefzadeh LRM 153 0 0 09 May 2025
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving Qi Liu Xinhao Zheng Renqiu Xia Xingzhi Qi Qinxiang Cao Junchi Yan AIMat 140 0 0 07 May 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 79 0 0 27 Apr 2025
APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries Huajian Xin Luming Li Xiaoran Jin Jacques Fleuriot Wenda Li AIMat 151 0 0 27 Apr 2025
Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification Balaji Rao William Eiers Carlo Lipizzi 153 0 0 23 Apr 2025
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning Haiming Wang Mert Unsal Xiaohan Lin Mantas Baksys Qingbin Liu ... Zhouliang Yu Ziyi Wang Zhilin Yang Zhengying Liu Jia-Nan Li AIMat ReLM AI4TS LRM 156 18 0 15 Apr 2025
SkillWeaver: Web Agents can Self-Improve by Discovering and Honing Skills Boyuan Zheng Michael Y. Fatemi Xiaolong Jin Ziyi Wang Apurva Gandhi ... Yu Gu Jayanth Srinivasa Gaowen Liu Graham Neubig Yu Su CLL 137 11 0 09 Apr 2025
Lemmanaid: Neuro-Symbolic Lemma Conjecturing Yousef Alhessi Sólrún Halla Einarsdóttir George Granberry Emily First Moa Johansson Sorin Lerner Nicholas Smallbone 59 2 0 07 Apr 2025
Attention-Aware Multi-View Pedestrian Tracking Reef Alturki Adrian Hilton Jean-Yves Guillemaut 88 0 0 03 Apr 2025
Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving Sara Rajaee Kumar Pratik Gabriele Cesa Arash Behboodi OffRL LRM 125 0 0 12 Mar 2025
From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems Zekun Zhou Xiaocheng Feng L. Huang Xiachong Feng Ziyun Song ... Baoxin Wang Dayong Wu Guoping Hu Ting Liu Bing Qin AI4TS 129 1 0 03 Mar 2025
CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization Shuming Shi Ruobing Zuo Gaolei He Jianlin Wang Chenyang Xu Zhengfeng Yang 127 0 0 25 Feb 2025
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques Sangjun Han Taeil Hur Youngmi Hur Kathy Sangkyung Lee Myungyoon Lee Hyojae Lim 525 0 0 20 Feb 2025
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity Dylan Zhang Justin Wang Tianran Sun 145 1 0 17 Feb 2025
ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data Xiaoyang Liu Kangjie Bao Jiashuo Zhang Yunqi Liu Yu Chen Yu Chen Yang Jiao Tao Luo AIMat 112 2 0 08 Feb 2025
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation Quinn Dougherty Ronak Mehta ALM 101 2 0 08 Feb 2025
Formal Mathematical Reasoning: A New Frontier in AI Kaiyu Yang Gabriel Poesia Jingxuan He Wenda Li Kristin Lauter Swarat Chaudhuri Dawn Song LRM AI4CE 165 36 0 20 Dec 2024
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification Kyle Thompson Nuno Saavedra Pedro Carrott Kevin Fisher Alex Sanchez-Stern Yuriy Brun J. Ferreira Sorin Lerner E. First LRM 244 4 0 18 Dec 2024
Inference Scaling fLaws: The Limits of LLM Resampling with Imperfect Verifiers Benedikt Stroebl Sayash Kapoor Arvind Narayanan LRM 160 18 0 26 Nov 2024
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically Kefan Dong Arvind V. Mahankali Tengyu Ma ReLM LRM 109 7 0 04 Nov 2024
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction Liao Zhang David M. Cerna C. Kaliszyk 59 0 0 02 Nov 2024
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency Zenan Li Yifan Wu Zhaoyu Li Xinming Wei Xian Zhang Fan Yang Xiaoxing Ma 91 8 0 28 Oct 2024
Library Learning Doesn't: The Curious Case of the Single-Use "Library" Ian Berlot-Attwell Frank Rudzicz Xujie Si 78 1 0 26 Oct 2024
Cobblestone: Iterative Automation for Formal Verification Saketh Ram Kasibatla Arpan Agarwal Yuriy Brun Sorin Lerner Talia Ringer Emily First 45 1 0 25 Oct 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Yeyun Gong Nan Duan Ping Wei AIMat 115 1 0 21 Oct 2024
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes Sean Lamont Christian J. Walder Amir Dezfouli Paul Montague Michael Norrish 91 0 0 14 Oct 2024
Mars: Situated Inductive Reasoning in an Open-World Environment Xiaojuan Tang Jiaqi Li Yitao Liang Song-chun Zhu Muhan Zhang Zilong Zheng LM&Ro LRM LLMAG 82 5 0 10 Oct 2024
Herald: A Natural Language Annotated Lean 4 Dataset Guoxiong Gao Yutong Wang Jiedong Jiang Qi Gao Zihan Qin Tianyi Xu Bin Dong 224 8 0 09 Oct 2024
Consistent Autoformalization for Constructing Mathematical Libraries Lan Zhang Xin Quan André Freitas AI4CE 72 4 0 05 Oct 2024
AutoVerus: Automated Proof Generation for Rust Code Chenyuan Yang Xuheng Li Md Rakib Hossain Misu Jianan Yao Weidong Cui ... Jacob R. Lorch Shuai Lu Fan Yang Ziqiao Zhou Shan Lu 111 11 0 19 Sep 2024
SubgoalXL: Subgoal-based Expert Learning for Theorem Proving Xueliang Zhao Lin Zheng Haige Bo Changran Hu Urmish Thakker Lingpeng Kong LRM 111 6 0 20 Aug 2024
Benchmarking Large Language Models for Math Reasoning Tasks Kathrin Seßler Yao Rong Emek Gözlüklü Enkelejda Kasneci LRM 63 4 0 20 Aug 2024
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search Huajian Xin Zhaochun Ren Junxiao Song Zhihong Shao Wanjia Zhao ... Dejian Yang Zhibin Gou Z. F. Wu Fuli Luo Chong Ruan AIMat LRM 149 70 0 15 Aug 2024
LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover Zijian Wu Jiayu Wang Dahua Lin Kai-xiang Chen 115 15 0 24 Jul 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 206 29 0 14 Jul 2024
GenArtist: Multimodal LLM as an Agent for Unified Image Generation and Editing Zhenyu Wang Aoxue Li Zhenguo Li Xihui Liu MLLM DiffM 132 40 0 08 Jul 2024
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving Xiaohan Lin Qingxing Cao Yinya Huang Haiming Wang Jianqiao Lu Zhengying Liu Linqi Song Xiaodan Liang LRM 55 9 0 20 Jun 2024
miniCodeProps: a Minimal Benchmark for Proving Code Properties Evan Lohn Sean Welleck 69 6 0 16 Jun 2024
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data Huajian Xin Daya Guo Zhihong Shao Zhaochun Ren Qihao Zhu Bo Liu Chong Ruan Wenda Li Xiaodan Liang SyDa 116 91 0 23 May 2024
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Saikat Chakraborty Gabriel Ebner Siddharth Bhat Sarah Fakhoury Sakina Fatima Shuvendu K. Lahiri Nikhil Swamy 92 16 0 03 May 2024
A Survey on Deep Learning for Theorem Proving Zhaoyu Li Jialiang Sun Logan Murphy Qidong Su Zenan Li Xian Zhang Kaiyu Yang Xujie Si LRM 125 32 0 15 Apr 2024