@inproceedings{
welleck2023llmstep,
title={llmstep: {LLM} proofstep suggestions in Lean},
author={Sean Welleck and Rahul Saha},
booktitle={The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23},
year={2023},
url={https://openreview.net/forum?id=ODOJuAM4Qj}
}
We present $\texttt{llmstep}$, a tool for suggesting proof steps with a language model in the Lean 4 proof assistant. $\texttt{llmstep}$ is a Lean 4 tactic that sends a user's proof state to a server hosting a language model. The language model generates suggestions, which are checked in Lean and displayed to a user in their development environment. We provide a baseline language model, along with code for fine-tuning and evaluation to support further development. We provide server implementations that run on CPU, a CUDA GPU, or a Google Colab notebook, as a step towards fast, effective language model suggestions for any user.
llmstep: LLM proofstep suggestions in Lean
Sean Welleck Rahul Saha