Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

6 June 2024

Jiayu Wang

Kai Chen

Papers citing "Lean Workbook: A large-scale Lean problem set formalized from natural language math problems"

21 / 21 papers shown

Title
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 2 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 14 0 0 16 May 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 33 0 0 27 Apr 2025
Leanabell-Prover: Posttraining Scaling in Formal Reasoning Jingyuan Zhang Qi Wang Xingguang Ji Yong Liu Yang Yue Fuzheng Zhang Di Zhang Guorui Zhou Kun Gai LRM 44 4 0 08 Apr 2025
Rosetta-PL: Propositional Logic as a Benchmark for Large Language Model Reasoning Shaun Baek Shaun Esua-Mensah Cyrus Tsui Sejan Vigneswaralingam Abdullah Alali Michael Lu Vasu Sharma Sean O'Brien Kevin Zhu LRM 58 0 0 25 Mar 2025
FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4 Jiarui Yao Ruida Wang Tong Zhang LRM 65 0 0 05 Mar 2025
MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving Ruida Wang Rui Pan Yuxin Li Jipeng Zhang Yizhen Jia Shizhe Diao Renjie Pi Junjie Hu Tong Zhang LRM LLMAG 92 6 0 05 Mar 2025
SURGE: On the Potential of Large Language Models as General-Purpose Surrogate Code Executors Bohan Lyu Siqiao Huang Zichen Liang Qi-An Sun Jiaming Zhang ELM LRM 60 0 0 16 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 55 0 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 82 21 0 20 Dec 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 45 0 0 21 Oct 2024
Herald: A Natural Language Annotated Lean 4 Dataset Guoxiong Gao Yutong Wang Jiedong Jiang Qi Gao Zihan Qin Tianyi Xu Bin Dong 88 3 0 09 Oct 2024
Can Transformers Do Enumerative Geometry? Baran Hashemi Roderic G. Corominas Alessandro Giacchetto 44 2 0 27 Aug 2024
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search Huajian Xin Z. Z. Ren Junxiao Song Zhihong Shao Wanjia Zhao ... Dejian Yang Zhibin Gou Z. F. Wu Fuli Luo Chong Ruan AIMat LRM 50 51 0 15 Aug 2024
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts Ruida Wang Jipeng Zhang Yizhen Jia Rui Pan Shizhe Diao Renjie Pi Tong Zhang LRM 35 16 0 03 Jul 2024
Process-Driven Autoformalization in Lean 4 Jianqiao Lu Zhengying Liu Yingjia Wan Yinya Huang Haiming Wang Zhicheng YANG Jing Tang Zhijiang Guo AI4CE 42 14 0 04 Jun 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 50 21 0 15 Apr 2024
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 73 158 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 110 157 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 89 116 0 03 Feb 2022
Chain-of-Thought Prompting Elicits Reasoning in Large Language Models Jason W. Wei Xuezhi Wang Dale Schuurmans Maarten Bosma Brian Ichter F. Xia Ed H. Chi Quoc Le Denny Zhou LM&Ro LRM AI4CE ReLM 395 8,495 0 28 Jan 2022