# LLMSTEP: LLM proofstep suggestions in Lean

arXiv: https://arxiv.org/abs/2310.18457 · HTML: https://mlsanity.com/paper/2310.18457/

## Key facts

- Cited by 32 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 17 references that are in the map.
- First posted on arXiv 27 Oct 2023.

## Builds on (most cited first, 9 of 9)

- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Pythia: A Suite for Analyzing Large Language Models Across Training and Scaling](https://mlsanity.com/paper/2304.01373/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [QED at Large: A Survey of Engineering of Formally Verified Software](https://mlsanity.com/paper/2003.06458/) (2020)

## Built on by (most cited first, 30 of 32)

- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models](https://mlsanity.com/paper/2406.16838/) (2024)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning](https://mlsanity.com/paper/2402.06332/) (2024)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective](https://mlsanity.com/paper/2501.11110/) (2025)
- [Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers](https://mlsanity.com/paper/2509.06493/) (2025)
- [Mathematical Language Models: A Survey](https://mlsanity.com/paper/2312.07622/) (2023)
- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [miniCodeProps: a Minimal Benchmark for Proving Code Properties](https://mlsanity.com/paper/2406.11915/) (2024)
- [REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning](https://mlsanity.com/paper/2505.20613/) (2025)
- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations](https://mlsanity.com/paper/2505.24264/) (2025)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods](https://mlsanity.com/paper/2406.15540/) (2024)
- [Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast](https://mlsanity.com/paper/2411.02318/) (2024)
- [Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation](https://mlsanity.com/paper/2410.15748/) (2024)
- [Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization](https://mlsanity.com/paper/2501.13959/) (2025)
- [Steering LLMs for Formal Theorem Proving](https://mlsanity.com/paper/2502.15507/) (2025)
- [ProofCompass: Enhancing Specialized Provers with LLM Guidance](https://mlsanity.com/paper/2507.14335/) (2025)
- [Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving](https://mlsanity.com/paper/2503.09730/) (2025)
- [Clarifying Before Reasoning: A Coq Prover with Structural Context](https://mlsanity.com/paper/2507.02541/) (2025)
- [ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving](https://mlsanity.com/paper/2502.04671/) (2025)
- [Hierarchical Attention Generates Better Proofs](https://mlsanity.com/paper/2504.19188/) (2025)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition](https://mlsanity.com/paper/2510.11944/) (2025)

## Abstract (arXiv)

We present LLMSTEP, a tool for integrating a language model into the Lean proof assistant. 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.