Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
Proofs

Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

21 October 2022

Albert Q. Jiang

Timothée Lacroix

Guillaume Lample

Papers citing "Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs"

16 / 16 papers shown

Title
CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics J. Liu Xiaohan Lin Jonas Bayer Yael Dillies Weijie Jiang ... Zhengfeng Yang J. Zhang Lihong Zhi J. Li Zhengying Liu 33 0 0 06 May 2025
Towards Automated Scoping of AI for Social Good Projects Jacob Emmerson Rayid Ghani Zheyuan Ryan Shi 38 0 0 28 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
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 21 0 0 27 Apr 2025
Generative Evaluation of Complex Reasoning in Large Language Models Haowei Lin X. Wang Ruilin Yan Baizhou Huang Haotian Ye Jianhua Zhu Zihao Wang James Y. Zou Jianzhu Ma Yitao Liang ReLM ELM LRM 73 0 0 03 Apr 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 55 0 0 20 Feb 2025
Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions Lan Zhang Marco Valentino André Freitas 33 0 0 17 Feb 2025
Mathematical Language Models: A Survey W. Liu Hanglei Hu Jie Zhou Yuyang Ding Junsong Li ... Mengliang He Qin Chen Bo Jiang Aimin Zhou Liang He LRM 62 12 0 03 Jan 2025
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 90 1 0 18 Dec 2024
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 Leni Aniva Chuyue Sun Brando Miranda Clark W. Barrett Sanmi Koyejo 24 4 0 21 Oct 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 28 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 21 3 0 09 Oct 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 58 22 0 14 Jul 2024
ChartX & ChartVLM: A Versatile Benchmark and Foundation Model for Complicated Chart Reasoning Renqiu Xia Bo-Wen Zhang Hancheng Ye Xiangchao Yan Qi Liu ... Min Dou Botian Shi Junchi Yan Junchi Yan Yu Qiao LRM 35 50 0 19 Feb 2024
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 108 107 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 55 115 0 03 Feb 2022