Machine-Learned Premise Selection for Lean

17 March 2023

Papers citing "Machine-Learned Premise Selection for Lean"

8 / 8 papers shown

Title
LeanAgent: Lifelong Learning for Formal Theorem Proving Adarsh Kumarappan Mo Tiwari Peiyang Song Robert Joseph George Chaowei Xiao Anima Anandkumar CLL LLMAG LRM 74 8 0 08 Oct 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 42 25 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 40 4 0 06 Mar 2024
Rigor with Machine Learning from Field Theory to the Poincaré Conjecture Sergei Gukov James Halverson Fabian Ruehle AI4CE 47 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 17 10 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 38 216 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 52 44 0 08 Mar 2023
MizAR 40 for Mizar 40 C. Kaliszyk Josef Urban VLM AI4CE LRM AIMat 61 133 0 10 Oct 2013