REVIEW 11 cited by
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Not yet reviewed by Pith; the record is open.
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
read the original abstract
Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: an open-source Lean playground consisting of toolkits, data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection: a key bottleneck in theorem proving. Using this data, we develop ReProver (Retrieval-Augmented Prover): an LLM-based prover augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. Furthermore, we construct a new benchmark consisting of 98,734 theorems and proofs extracted from Lean's math library. It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research.
Forward citations
Cited by 11 Pith papers
-
DualityCert: Verifier-Gated Language-Model Repair of Broken Duality Claims in Quantum Field Theory
Verifier-gated LM repair improves success on broken quiver-gauge-theory claims, but the best exploitation policy reverses between deepseek-chat and qwen-plus.
-
TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation
An exact model-checker oracle for NL-to-TLA+ still yields an elevenfold “correctness envelope” (18.7%–1.7%) once interface supply and vacuity screens are made explicit.
-
DINGO: Constrained Inference for Diffusion LLMs
DINGO is a dynamic programming decoder over a token-level DFA that makes diffusion LLM outputs obey regular expressions while maximizing the product of per-position probabilities.
-
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
Lean-auto translates Lean 4 goals into higher-order logic for external theorem provers, and on Mathlib4 it solves 36.6% of 149,142 test theorems with Duper, ahead of existing tactics.
-
AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis
AutoCedar first builds a reviewed, checkable authorization boundary from natural-language requirements, then synthesizes Cedar policies against that fixed target with verifier-guided repair, solving all 221 CedarBench tasks.
-
An AI Approach to Verified Production Cryptographic Libraries
An AI agent, guarded by mechanical integrity gates, synthesized Verus-verified internal specifications and proofs for curve25519-dalek and chacha20 without changing executable code.
-
Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
A verifier-grounded self-evolving Lean proof agent with a champion-driven, self-hardening benchmark reached 45.1% held-out miniF2F solve rate versus 32.0% for a fixed-benchmark baseline.
-
Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning
A taxonomy-guided ensemble of LLM judges correlates with human ratings of autoformalizations (up to 0.662 on Isabelle/HOL) better than coarse-grained judges and reference metrics, but validation is partly in-sample an...
-
Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration
Albilich, an agentic math-research harness with persistent proof state, CAS integration, and an advisor role, reports 10/10 RealMath solves and two Kourovka results, but with no public artifacts or independent verification.
-
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Workflow control and a cached Lean verifier improve completion and token efficiency in document-to-project autoformalization.
-
Grain Theory: Type-Level Granularity Correctness in Data Pipelines
A formal notion of 'grain' (a minimal identifying type) is defined and used to infer the grain of join results from input grains, claiming compile-time verification of pipeline correctness.
Discussion (0). Continue with ORCID to comment.