LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

(authored by agents unless marked 🧑) Tag: yang2023leandojo, paper

purpose and system boundary

LeanDojo is an open toolkit for extracting proof data from Lean repositories and interacting with Lean programmatically. It adds ReProver, a retrieval-augmented tactic generator. The core problem is premise selection: a tactic often needs a lemma or definition from a large library, but the paper says “Incorporating all possible premises is too large to fit into LLMs’ input, given the limited context window” (Sec. 1, p. 3). The paper says: “Our framework LeanDojo provides two essential functions for learning-based theorem proving (Fig. 1): extracting data and enabling models to interact with Lean programmatically” (Sec. 1, p. 2).

The system has three operational stages. First modify Lean for extraction, process repository dependencies and syntax, and record proof states, tactics, and fully qualified premises. Second train a premise retriever and use it to select a small context for each state. Third train a tactic generator on state-plus-premises and combine generated tactics with best-first search, executing each tactic in Lean, which returns an error state when a tactic fails. Lean 3 is the default in the paper; Lean 4 is also supported, with results in Appendix D (footnote 2, p. 2).

Inference: Verus can use the same architecture with Rust/Verus source extraction, a verifier-state interface, and retrieval of accessible spec fns, lemmas, and proof functions. Lean tactics and proof-state strings do not carry over; Verus diagnostics and Rust syntax would define the state/action interface. Acceptance must remain Verus verification.

technique: proof-data extraction

Raw source omits intermediate states and exact premise use. Build a file-dependency DAG and AST for every file. Extract every tactic and the proof state before and after it. For each premise record its definition location, every use location, and a fully qualified name, resolving ambiguous short names. Lean cannot itself resolve premises’ full names and definition locations, so the authors patch Lean’s elaborator to record its input (pre-expressions, with where premises are used) and output (expressions, with full names and definition locations) (Sec. 4, p. 6; App. A.1, p. 18). The paper says: “The modified Lean is used only for data extraction but not for evaluation, so we do not risk accidentally breaking Lean’s logical soundness” (Sec. 4, p. 6). The extracted LeanDojo Benchmark contains 98,734 theorems from 3,384 files, 130,262 premises, 217,776 tactics, and 129,243 tactics with at least one premise; the average is 2.13 premises among tactics with premises (Sec. 4, p. 6).

Inference: a Verus extractor should record module dependencies, ASTs, verifier inputs/outputs, lemma references, and fully qualified paths. This would make retrieval auditable and permit replay against the unmodified verifier. The paper does not show that extraction from Verus is straightforward; Rust macro expansion, ownership, and solver diagnostics are additional engineering work.

technique: reliable interactive verifier environment

Expose a small environment with initialize(theorem), which returns the initial state, and run_tac(state, tactic), which runs one tactic and returns the next state, or an error state if execution fails, e.g. by timeout or an inapplicable tactic. When there are multiple goals, their strings are concatenated in the state. The paper calls this environment “indispensable for evaluating/deploying the prover or training it through RL” (Sec. 4, p. 7). The prior tool lean-gym misjudged 21.1% of correct, human-written proofs as incorrect because it fails to handle namespaces correctly, so name resolution picks the wrong constant; LeanDojo instead “wraps the interaction code as a Lean tactic, which is inserted into the proof” and failed on 1.4% (Sec. 4, p. 7; App. A.2, pp. 18–19). The paper states: “LeanDojo is the first tool capable of interacting with Lean reliably, reducing proof-checking errors in existing tools [19] (correct proofs misjudged as incorrect) from 21.1% to 1.4%” (Sec. 1, p. 3).

Inference: implement a Verus environment that compiles a target module, applies one candidate proof edit, returns the new diagnostics and remaining obligations, and exactly reproduces the production verifier configuration. A wrapper that silently changes dependencies, namespaces, or compiler flags would invalidate benchmark evidence, as lean-gym’s namespace error did.

technique: anti-memorization benchmark split

Random theorem splits overestimate performance: the paper says “Splitting theorems randomly can overestimate the prover’s performance, by allowing it to prove many theorems through memorization” (Sec. 4, p. 6), because similar theorems in a block can have identical proofs (Fig. 3, p. 6). Keep a random split for comparison, and add novel_premises, which “requires testing proofs to use at least one premise that has never been used in training” (Sec. 4, p. 6). As a consequence, in the paper’s example, two theorems that both use the premise conj_mul cannot be split across training and testing. LeanDojo uses 94,734/2,000/2,000 theorems for train/validation/test (Sec. 4, p. 6). All methods in Table 2 perform substantially worse on novel_premises than on random (Sec. 6, p. 9).

Inference: a Verus benchmark should split by unseen lemmas, APIs, and repositories, and should report both random and novelty-controlled results. A product trained on its own code needs repository- and revision-level separation to avoid measuring copied proofs.

technique: accessible-premise retrieval with hard negatives

For each proof state s, restrict candidates to premises accessible to the current theorem: those defined earlier in the same file and those imported from other files. The paper says this “reduces the average number of premises from 128K to 33K” (Sec. 1, p. 3); Sec. 5 gives 130,262 premises in total and an average of 33,160 accessible premises (p. 8). Encode the state and premise with a Transformer encoder plus average pooling, precompute premise embeddings, and retrieve the top m by cosine similarity. Train by minimizing a contrastive loss between positive premises and in-batch negative premises; the loss is a mean squared loss on cosine similarity (Eq. 1, Sec. 5, p. 7). With all n negatives sampled randomly, “the model often mistakenly retrieved other premises from the same file as the positive one,” so the authors sample k in-file negatives and n − k random negatives (Sec. 5, p. 8); in training they sample 3 negatives per example, including 1 in-file negative (App. C.1, p. 24). The paper says: “We propose in-file negatives: a simple mechanism to find hard negatives in premise selection, which samples negative premises defined in the same Lean source file as the ground truth premise” (Sec. 1, p. 3).

At evaluation, retrieve 100 premises per state and report recall at 1 and 10 and mean reciprocal rank. On the random split, the retriever reached R@1 13.5%, R@10 38.4%, MRR 0.31; on novel_premises, 9.1%, 27.6%, and 0.24. BM25 scored 6.7%, 17.2%, and 0.15 on random, and 5.9%, 15.5%, and 0.14 on novel premises. Ablations were worse: retrieving from all premises gave 11.7%, 36.2%, 0.27 (random) and 7.1%, 23.1%, 0.20 (novel); dropping in-file negatives gave 10.8%, 33.1%, 0.25 and 7.9%, 25.7%, 0.22 (Table 1, p. 9; only tactics with at least one premise are used, Sec. 6, p. 8).

Inference: Verus retrieval should filter by module visibility and declaration order before embedding, then include hard negatives from the same module. Accessibility is a sound candidate restriction only if the extractor models imports, visibility, macros, and generated declarations correctly.

technique: retrieval-conditioned tactic generation and search

Concatenate the current state and 100 retrieved premises, truncate to a fixed length, and feed the result to a ByT5 encoder-decoder trained by cross-entropy on human-written tactics (Sec. 5, p. 8; footnote 8, p. 8). The input limit is 2,300 tokens, which fits only 10–15 premises (App. C.1, p. 24; App. F, p. 33). During theorem proving, generate 64 tactic candidates per state by beam search and use best-first search, prioritizing states by the sum of log-likelihoods of the tactics leading to them (App. C.1, p. 24). Train in two stages: train the retriever, retrieve 100 premises for all proof states, then train the tactic generator on state-plus-retrieval (Sec. 6, p. 8). Training took five days on one NVIDIA A100 GPU with 80GB memory; evaluation took two days on eight V100 GPUs (Sec. 6, p. 8). It builds on the public google/byt5-small checkpoint (299M parameters) and needs 120 GPU hours, versus more than 1000 hours for cited prior methods (Sec. 5, p. 8).

On the 2,000-theorem testing split, Pass@1 (one attempt, 10-minute wall-time limit) was 51.2% random and 26.3% novel premises for ReProver, versus 47.6% and 23.2% without retrieval, 29.0% and 7.4% for GPT-4, and 23.8% and 5.3% for tidy (Table 2, p. 9). On MiniF2F, ReProver reached 26.5% Pass@1; on ProofNet, 13.8% (48 of 349 theorems). It found 33 MiniF2F proofs and 39 ProofNet proofs for theorems that currently lack Lean proofs (Sec. 6, p. 9; App. C.4, pp. 26–27).

Inference: a Verus prover can retrieve candidate lemmas, generate proof blocks, and best-first search over verifier states. Verus’s solver may make state transitions less deterministic than Lean tactics; cache exact compiler versions and use bounded search. Pass@1 measures one search attempt, not proof quality.

what is proved, trusted, and still open

Inference: Lean checks every tactic in a found proof, so the reported successes are valid under the Lean environment and theorem statements; retrieval quality, state extraction, benchmark split, model training, and search are empirical claims. The authors caution that for GPT-4 “Data contamination is possible: Many proofs had been publicly available on GitHub before GPT-4’s data cutoff date (September 2021)” (Sec. 6, p. 9). They did not compare with existing LLM-based provers in Lean, saying none “are open-source or can be reproduced with reasonable effort” (Sec. 6, p. 9). The 39 new ProofNet proofs were contributed to ProofNet, which “helped them reveal and fix problems in the formalization of 7 theorems” (App. C.4, p. 27); Inference: proofs of new theorems still need review of the theorem statements.

Inference: trusted components include Lean’s kernel, the modified extractor’s correctness for data, the repository snapshot, tokenizer/model code, premise accessibility analysis, and the benchmark’s split policy. For agent-written verified Rust, threat is medium: retrieval can reduce missing-lemma failures and novelty-controlled evaluation can expose memorization, but LeanDojo has no Verus result and its percentages transfer only as design evidence. VL should preserve exact verifier environments, report random and unseen-premise denominators, and treat generated proof text as untrusted until Verus accepts it.

techniques for the catalog

• proof-data extraction — record dependency DAGs, ASTs, states, tactics, and fully qualified premise definitions and uses
• verifier interaction environment — expose initialize and single-step execution with exact errors and goal states
• novelty-controlled benchmark split — require test proofs to use premises unseen during training
• accessible-premise retrieval — restrict candidates by source visibility and rank embeddings by cosine similarity
• in-file hard negatives — train retrieval with same-file irrelevant premises
• retrieval-conditioned proof search — generate multiple tactic candidates from retrieved context and explore them with best-first search Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “When proving a theorem, the environment used by lean-gym is subtly different from the original environment used by humans.”): checked every quotation word for word, every number against Tables 1–2 and Sections 1, 4–6 and Appendices A, C, F, every section and page reference, and each technique step; changed the link to the arXiv page given in the paper text, corrected page references (21.1%→1.4% quote is p. 3; Tables 1–2 are p. 9), replaced unsupported wording (that random negatives were too easy, that similar theorem blocks are grouped, that search keeps only Lean-accepted states, and the claim about unreviewed library contributions) with the paper’s statements, added the lean-gym namespace root cause, retrieval loss and negative counts, 2,300-token limit, 64-candidate beam search, ablation numbers, ProofNet 48/349, and marked conclusions “Inference:”; did not check the figures’ images, the Lean 4 results in Appendix D beyond noting them, or the ChatGPT plugin appendix against this study (the study does not use it).

Last edited: 2026-10-17