Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean

18 April 2024

Papers citing "Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean"

9 / 9 papers shown

Title
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning Azim Ospanov Farzan Farnia Roozbeh Yousefzadeh LRM 26 0 0 09 May 2025
Optimization Problem Solving Can Transition to Evolutionary Agentic Workflows Wenhao Li Bo Jin Mingyi Hong Changhong Lu Xiangfeng Wang 46 0 0 07 May 2025
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity Dylan Zhang Justin Wang Tianran Sun 36 0 0 17 Feb 2025
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 40 0 0 21 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 58 6 0 05 Aug 2024
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 59 92 0 08 Mar 2023
Magnushammer: A Transformer-Based Approach to Premise Selection Maciej Mikuła Szymon Tworkowski Szymon Antoniak Bartosz Piotrowski Albert Qiaochu Jiang Jinyi Zhou Christian Szegedy Lukasz Kuciñski Piotr Milo's Yuhuai Wu 39 42 0 08 Mar 2023
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