Pith. sign in

REVIEW 2 cited by

LLMSTEP: LLM proofstep suggestions in Lean

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2310.18457 v1 pith:3XC6CFTN submitted 2023-10-27 cs.AI cs.LG

Sean Welleck , Rahul Saha This is my paper
classification cs.AIcs.LG
keywords languagemodelleanllmstepsuggestionsuserdevelopmentproof
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. OpenAlex reports about 3 citations worldwide. Full citation record

  1. What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus

    cs.SE 2025-08 conditional novelty 6.0 of 10

    A user study of eight experts shows that specification-first planning, low active errors, and measured verifier use predict proof task success, informing an AI proof agent design.

  2. Clarifying Before Reasoning: A Coq Prover with Structural Context

    cs.AI 2025-07 reject novelty 5.0 of 10

    Enriching LLM theorem-proving prompts with Coq's internal type representations and natural-language explanations raises proof success from 21.8% to 45.8%, surpassing Graph2Tac's 33.2%.

Pith tools