mlsanityData to 7 Oct 2026

LLMSTEP: LLM proofstep suggestions in Lean

arXiv 2310.18457 ↗First posted 27 Oct 2023cs.AI cs.LGcited by 32

Not on the map. Why?

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.

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

Builds on

9 of 17 references.

References · 9

  1. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,767
  2. 2023Pythia: A Suite for Analyzing Large Language Models Across Training and Scalingcited by 1,734
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  4. 2023Llemma: An Open Language Model For Mathematicscited by 385
  5. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  6. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  7. 2019The Lean mathematical librarycited by 127
  8. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  9. 2020QED at Large: A Survey of Engineering of Formally Verified Softwarecited by 13

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 1; 2024: 12; 2025: 15; 2026: 4.

32 papers.

Sort:

By area:

  1. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  2. 2024From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Modelscited by 136
  3. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 117
  4. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  5. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  6. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  7. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  8. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  9. 2025Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspectivecited by 29
  10. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  11. 2023Mathematical Language Models: A Surveycited by 24
  12. 2026Large Language Model Reasoning Failurescited by 20
20 more
  1. 2024miniCodeProps: a Minimal Benchmark for Proving Code Propertiescited by 18
  2. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  3. 2025LeanExplore: A search engine for Lean 4 declarationscited by 13
  4. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 9
  5. 2025Faithful and Robust LLM-Driven Theorem Proving for NLI Explanationscited by 8
  6. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
  7. 2024Specify What? Enhancing Neural Specification Synthesis by Symbolic Methodscited by 6
  8. 2024Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFastcited by 5
  9. 2025Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalizationcited by 4
  10. 2025Steering LLMs for Formal Theorem Provingcited by 4
  11. 2024Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutationcited by 3
  12. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidancecited by 3
  13. 2025Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Provingcited by 2
  14. 2025ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Provingcited by 1
  15. 2025Hierarchical Attention Generates Better Proofscited by 1
  16. 2025Clarifying Before Reasoning: A Coq Prover with Structural Contextcited by 1
  17. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  18. 2025TopoAlign: A Framework for Aligning Code to Math via Topological Decompositioncited by 0
  19. 2026Automating Formal Verification with Agent-Guided Tree Searchcited by 0
  20. 2026An Empirical Study of LLM-Generated Specifications for VeriFastcited by 0