LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN
prover

LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover

24 July 2024

Dahua Lin

ArXiv (abs)PDF HTML

Papers citing "LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover"

15 / 15 papers shown

Title
Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training Xinyuan Zhou Yi Lei Xiaoyu Zhou Jingyi Sun Yu Zhu Zhongyi Ye Weitai Zhang Quan Liu Si Wei Cong Liu ALM LRM 199 0 0 17 Nov 2025
GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving Ruida Wang Jiarui Yao Rui Pan Shizhe Diao Tong Zhang 59 0 0 13 Oct 2025
Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers Ran Xin Zeyu Zheng Yanchen Nie Kun Yuan Xia Xiao OffRL LRM 138 2 0 08 Sep 2025
Automated Formalization via Conceptual Retrieval-Augmented LLMs Wangyue Lu Lun Du Sirui Li Ke Weng Haozhe Sun Hengyu Liu Minghe Yu Tiancheng Zhang Ge Yu 120 3 0 09 Aug 2025
Solving Formal Math Problems by Decomposition and Iterative Reflection Yichi Zhou Jianqiu Zhao Yongxin Zhang Bohan Wang Siran Wang ... Rong Ye Phan Nhat Hoang Huishuai Zhang Peng Sun Hang Li 115 13 0 21 Jul 2025
Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs Kaito Baba Chaoran Liu Shuhei Kurita Akiyoshi Sannai LLMAG 280 9 0 24 Jun 2025
STORM-BORN: A Challenging Mathematical Derivations Dataset Curated via a Human-in-the-Loop Multi-Agent FrameworkAnnual Meeting of the Association for Computational Linguistics (ACL), 2025 Wenhao Liu Zhenyi Lu Xinyu Hu Jierui Zhang Dailin Li ... Pei Zhang Chengbo Zhang Yuxiang Ren Xiaohong Huang Yan Ma OffRL 226 3 0 02 Jun 2025
Leanabell-Prover: Posttraining Scaling in Formal Reasoning Jingyuan Zhang Qi Wang Xingguang Ji Wenshu Fan Yang Yue Fuzheng Zhang Di Zhang Guorui Zhou Kun Gai LRM 422 18 0 08 Apr 2025
From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support SystemsConference on Empirical Methods in Natural Language Processing (EMNLP), 2025 Zekun Zhou Xiaocheng Feng Daigang Xu Xiachong Feng Ziyun Song ... Baoxin Wang Dayong Wu Guoping Hu Ting Liu Bing Qin AI4TS 392 7 0 03 Mar 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 284 12 0 08 Feb 2025
Alchemy: Amplifying Theorem-Proving Capability through Symbolic MutationInternational Conference on Learning Representations (ICLR), 2024 Shaonan Wu Shuai Lu Yeyun Gong Nan Duan Ping Wei AIMat 251 1 0 21 Oct 2024
LLM The Genius Paradox: A Linguistic and Math Expert's Struggle with Simple Word-based Counting Problems Nan Xu Xuezhe Ma LRM 332 5 0 18 Oct 2024
SubgoalXL: Subgoal-based Expert Learning for Theorem Proving Xueliang Zhao Lin Zheng Haige Bo Changran Hu Urmish Thakker Lingpeng Kong LRM 229 12 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 247 124 0 15 Aug 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 236 42 0 15 Apr 2024