REVIEW 12 cited by
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
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
Neural theorem proving combines large language models (LLMs) with proof assistants such as Lean, where the correctness of formal proofs can be rigorously verified, leaving no room for hallucination. With existing neural theorem provers pretrained on a fixed collection of data and offering valuable suggestions at times, it is challenging for them to continually prove novel theorems in a fully autonomous mode, where human insights may be critical. In this paper, we explore LLMs as copilots that assist humans in proving theorems. We introduce Lean Copilot, a general framework for running LLM inference natively in Lean. It enables programmers to build various LLM-based proof automation tools that integrate seamlessly into the workflow of Lean users. Lean users can use our pretrained models or bring their own ones that run either locally (with or without GPUs) or on the cloud. Using Lean Copilot, we build LLM-based tools that suggest proof steps, complete proof goals, and select relevant premises. Experimental results on the Mathematics in Lean textbook demonstrate the effectiveness of our method compared to existing rule-based proof automation in Lean (aesop). When assisting humans, Lean Copilot requires only 2.08 manually-entered proof steps on average (3.86 required by aesop); when automating the theorem proving process, Lean Copilot automates 74.2% proof steps on average, 85% better than aesop (40.1%). We open source all code and artifacts under a permissive MIT license to facilitate further research.
Forward citations
Cited by 12 Pith papers
-
CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
CausalForge is a Lean-grounded, self-improving agentic framework that proposes, proves, and statement-audits causal inference theorems; its runs produced nine accepted results including a new ATE minimax upper bound.
-
No Certificate, No Categorical Speech Act: A Brouwerian Assertibility Constraint for Public Reason
An AI may assert or deny high-stakes claims only when it can exhibit a publicly contestable certificate; otherwise it is obligated to return Undetermined.
-
CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
CircuitProver is an agentic Lean 4 framework that automatically proves parameterized hardware designs correct against formalized specifications and reuses proof knowledge across tasks.
-
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.
-
What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
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.
-
Unveiling Causal Reasoning in Large Language Models: Reality or Mirage?
LLMs perform much worse on causal questions built from post-cutoff news articles, suggesting their apparent causal skill is mostly memorization, and a general-knowledge prompt method only partly closes the gap.
-
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.
-
Creativity in LLM-based Multi-Agent Systems: A Survey
A taxonomy-driven survey organizes the emerging field of creativity in LLM-based multi-agent systems across workflows, techniques, personas, datasets, and evaluation metrics.
-
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
ProofWala is a multilingual proof-engineering framework that demonstrates cross-lingual transfer between Lean 4 and Coq for neural theorem proving.
-
Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
An integrated survey organizing AI mathematical reasoning into informal, formal, discovery, and technique axes while cataloging benchmarks and assessing failure modes.
-
Formally Solving Answer-Construction Problems in Lean
ECP, an enumerate-conjecture-prove framework with Lean verification, improves answer-construction accuracy on ConstructiveBench and a PutnamBench subset, but its benchmark has a 17% major-error rate and its abstract r...
-
A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry
Retrieving analogous solved geometry problems and adding a symbolic verifier's feedback lifts reported LLM formal proof accuracy from 10-44% to 68-96% on SAT-level problems, though the evaluation may include the targe...
Discussion (0). Continue with ORCID to comment.