Title
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving Qi Liu Xinhao Zheng Renqiu Xia Xingzhi Qi Qinxiang Cao Junchi Yan AIMat 45 0 0 07 May 2025
FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models Zhouliang Yu Ruotian Peng Keyi Ding Y. K. Li Zhongyuan Peng ... Huajian Xin W. R. Huang Yandong Wen Ge Zhang Weiyang Liu LRM 64 0 0 05 May 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 26 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 48 0 0 27 Apr 2025
Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad Ivo Petrov Jasper Dekoninck Lyuben Baltadzhiev Maria Drencheva Kristian Minchev Mislav Balunović Nikola Jovanović Martin Vechev LRM ELM 62 8 0 27 Mar 2025
Satori: Reinforcement Learning with Chain-of-Action-Thought Enhances LLM Reasoning via Autoregressive Search Maohao Shen Guangtao Zeng Zhenting Qi Zhang-Wei Hong Zhenfang Chen Wei Lu G. Wornell Subhro Das David D. Cox Chuang Gan LLMAG LRM 106 5 0 04 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 82 20 0 20 Dec 2024
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency Zenan Li Yifan Wu Zhaoyu Li Xinming Wei Xian Zhang Fan Yang Xiaoxing Ma 32 3 0 28 Oct 2024
LeanAgent: Lifelong Learning for Formal Theorem Proving Adarsh Kumarappan Mo Tiwari Peiyang Song Robert Joseph George Chaowei Xiao Anima Anandkumar CLL LLMAG LRM 70 8 0 08 Oct 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 55 6 0 05 Aug 2024
Proving Olympiad Algebraic Inequalities without Human Demonstrations Chenrui Wei Mengzhou Sun Wei Wang LRM 42 6 0 20 Jun 2024
OlympicArena: Benchmarking Multi-discipline Cognitive Reasoning for Superintelligent AI Zhen Huang Zengzhi Wang Shijie Xia Xuefeng Li Haoyang Zou ... Yuxiang Zheng Shaoting Zhang Dahua Lin Yu Qiao Pengfei Liu ELM LRM 43 25 0 18 Jun 2024
Improving Autoformalization using Type Checking Auguste Poiroux Gail Weiss Viktor Kunčak Antoine Bosselut 37 2 0 11 Jun 2024
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems Huaiyuan Ying Zijian Wu Yihan Geng Jiayu Wang Dahua Lin Kai Chen 31 24 0 06 Jun 2024
Process-Driven Autoformalization in Lean 4 Jianqiao Lu Zhengying Liu Yingjia Wan Yinya Huang Haiming Wang Zhicheng YANG Jing Tang Zhijiang Guo AI4CE 37 14 0 04 Jun 2024
Proving Theorems Recursively Haiming Wang Huajian Xin Zhengying Liu Wenda Li Yinya Huang ... Zhicheng YANG Jing Tang Jian Yin Zhenguo Li Xiaodan Liang LRM 18 10 0 23 May 2024
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data Huajian Xin Daya Guo Zhihong Shao Z. Z. Ren Qihao Zhu Bo Liu Chong Ruan Wenda Li Xiaodan Liang SyDa 32 61 0 23 May 2024
Integrating Intent Understanding and Optimal Behavior Planning for Behavior Tree Generation from Human Instructions Xinglin Chen Yishuai Cai Yunxin Mao Minglong Li Wenjing Yang Weixia Xu Ji Wang 32 6 0 13 May 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 26 10 0 18 Apr 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 42 21 0 15 Apr 2024
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data Yinya Huang Xiaohan Lin Zhengying Liu Qingxing Cao Huajian Xin Haiming Wang Zhenguo Li Linqi Song Xiaodan Liang ALM 31 35 0 14 Feb 2024
Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challenges Qingyao Li Lingyue Fu Weiming Zhang Xianyu Chen Jingwei Yu Wei Xia Weinan Zhang Ruiming Tang Yong Yu AI4Ed ELM 27 17 0 27 Dec 2023
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models Jing Xiong Jianhao Shen Ye Yuan Haiming Wang Yichun Yin ... Yinya Huang Chuanyang Zheng Xiaodan Liang Ming Zhang Qun Liu AIMat LRM 16 15 0 16 Oct 2023
LEGO-Prover: Neural Theorem Proving with Growing Libraries Haiming Wang Huajian Xin Chuanyang Zheng Lin Li Zhengying Liu ... Enze Xie Jian Yin Zhenguo Li Heng Liao Xiaodan Liang LRM 39 61 0 01 Oct 2023
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs Albert Q. Jiang Sean Welleck Jin Peng Zhou Wenda Li Jiacheng Liu M. Jamnik Timothée Lacroix Yuhuai Wu Guillaume Lample AIMat 58 157 0 21 Oct 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 108 156 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 73 115 0 03 Feb 2022