Machine-Learned Premise Selection for Lean

v1v2 (latest)

Machine-Learned Premise Selection for Lean

17 March 2023

Bartosz Piotrowski

Ramon Fernández Mir

Edward W. Ayers

ArXiv (abs)PDF HTML

Papers citing "Machine-Learned Premise Selection for Lean"

8 / 8 papers shown

Title
Premise Selection for a Lean Hammer Thomas Zhu Joshua Clune Jeremy Avigad Albert Qiaochu Jiang Sean Welleck 27 0 0 09 Jun 2025
LeanAgent: Lifelong Learning for Formal Theorem Proving Adarsh Kumarappan Mo Tiwari Peiyang Song Robert Joseph George Chaowei Xiao Anima Anandkumar CLL LLMAG LRM 134 9 0 08 Oct 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 103 28 0 18 Apr 2024
Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubruv C. Kaliszyk Martin Suda Josef Urban LRM 93 5 0 06 Mar 2024
Rigor with Machine Learning from Field Theory to the Poincaré Conjecture Sergei Gukov James Halverson Fabian Ruehle AI4CE 81 16 0 20 Feb 2024
Graph2Tac: Online Representation Learning of Formal Math Concepts Lasse Blaauwbroek Miroslav Olšák Jason Rute F. I. S. Massolo Jelle Piepenbrock Vasily Pestun 94 11 0 05 Jan 2024
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models Kaiyu Yang Aidan M. Swope Alex Gu Rahul Chalamala Peiyang Song Shixing Yu Saad Godil R. Prenger Anima Anandkumar RALM 152 247 0 27 Jun 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 161 46 0 08 Mar 2023