PaperlayerView exact revision on arXiv

Source-linked AI summary

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean

Peiyang Song, Kaiyu Yang, Anima Anandkumar

arXiv:2404.12534v3cs.AIcs.LGcs.LOstat.ML

TL;DR

LLMs can struggle with novel theorems, while formal proof work also requires time-consuming routine effort, motivating assistance that leaves experts guiding the process. Lean Copilot runs LLM inference in Lean and provides tools for tactic suggestions, proof search, and premise selection. On Mathematics in Lean, it improves on AESOP in both assisted and automated proving, with 74.2% of proof steps automated on average.

  • Problem

    LLMs often fail on novel or challenging theorems, while mathematicians also spend time on routine Lean work such as looking up premise names.

    Source: §1 · p. 2

  • Method

    Lean Copilot runs LLM inference natively in Lean and provides tools for tactic suggestions, complete-proof search, and premise selection.

    Source: §1 · p. 3

  • Results

    On Mathematics in Lean, Lean Copilot automates 74.2% of proof steps on average, 85% better than AESOP (40.1%), and requires 2.08 manually entered proof steps on average versus AESOP’s 3.86.

    Source: §1 · p. 3, §6 · p. 10

  • Takeaways & Limitations

    The project makes its code and evaluation artifacts public to facilitate further research.

    Source: §1 · p. 3

    AESOP uses a fixed, problem-dependent rule set and cannot adaptively choose tactics for intermediate proof goals during search.

    Source: §4.2 · p. 7

Abstract

from arXiv · show

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.

1. Introduction

Lean Copilot addresses the difficulty of proving novel theorems autonomously by helping people with routine proof construction while they guide the process. It runs LLM inference natively in Lean and supplies proof tools whose textbook results outperform AESOP.

1. Introduction

  • Existing systems target fully autonomous proving, but LLMs often struggle with novel theorems, while mathematicians spend time on routine tasks such as finding premise names.The paper proposes a copilot that eases routine construction while experts guide the overall process.Source: §1 · p. 2
  • Lean Copilot runs LLM inference natively in Lean and provides tools for tactic suggestions, proof search, and premise selection.Users can also build tools through low-level text-to-text and text-to-vector interfaces, and run models locally or via a server.Source: Figure 1 · p. 2, §1 · p. 3
  • On Mathematics in Lean, SEARCH_PROOFS automates 74.2% of proof steps on average—85% higher than AESOP and 27% higher than SUGGEST_TACTICS.SEARCH_PROOFS combines tactic generation with proof search; the reported results also show it requires fewer manually entered tactics than the two baselines.Source: §1 · p. 3
  • The project releases its code and evaluation artifacts publicly, and its tools can be installed as a Lean package and run on most hardware.The paper presents this as supporting future research and wider use in the Lean community.Source: §1 · p. 3

2. Related Work & Preliminaries

Prior work spans neural proof generation and classical proof automation, but the paper identifies a gap in practical, open-source tools that run LLMs directly in proof assistants. Lean Copilot is presented as a general native-in-Lean framework for this use.

Neural Theorem Proving

  • Neural theorem-proving work covers premise selection, tactic suggestion, and complete-proof generation, with later approaches emphasizing Transformer-based language models.Some systems pair tactic generation with premise retrieval and proof search, while whole-proof generation uses synthetic data to address data scarcity.Source: §2 · pp. 3–4

Human-AI collaboration in Formal Mathematics

  • The paper identifies a lack of practical open-source tools for direct LLM use in proof assistants and presents native inference as necessary for in-environment human-AI collaboration.It claims to be the first to address that challenge with a general framework for running LLM inference natively in Lean.Source: §2 · p. 4

Automation within Proof Assistants

  • Classical proof automation includes domain-specific decision procedures and general search tactics such as AESOP, whose rules are manually configured and fixed during search.The cited machine-learning approaches include premise-selection hammers and tactic predictors using handcrafted features or conventional classifiers.Source: §2 · p. 4
  • Earlier neural or LLM-based proof-assistant efforts ran models in Python and requested inference from the assistant, rather than running LLMs natively in Lean.The paper contrasts this with its support for native inference in Lean.Source: §2 · p. 4

3. Lean Copilot: A General Framework for Running LLM Inference in Lean

Lean Copilot is designed to provide fast, low-compute LLM assistance within Lean’s normal workflow. It uses Lean’s foreign function interface to run model inference and retrieval, while allowing users to supply their own models.

3. Lean Copilot: A General Framework for Running LLM Inference in Lean

  • Lean Copilot runs LLMs natively through Lean’s foreign function interface, avoiding the inter-process overhead and extra setup of a Python-hosted model.Its automation tools take tactic form and integrate into Lean’s workflow as a package.Source: §3 · p. 5
  • Lean’s FFI lets Lean functions call C++ implementations compiled into a shared library and dynamically linked to Lean.The paper uses this mechanism to call model-inference functions from Lean.Source: §3 · p. 5
  • By default, Lean Copilot runs ReProver, a ByT5 encoder-decoder model, locally via CTranslate2 or on a server, using beam search to generate outputs.Decoding hyperparameters include temperature and the number of requested output sequences; tokenization is unnecessary because ByT5 operates directly on UTF-8 bytes.Source: §3 · p. 5
  • For premise retrieval, Lean Copilot encodes the proof goal and scores it against precomputed premise embeddings to rank candidate premises.The retriever’s forward pass is wrapped in C++ and called from Lean through FFI.Source: §3 · p. 5
  • Lean Copilot supports user-supplied models with minimal changes when wrappers expose the required generation and/or encoding APIs.The framework is intended to run efficiently on most hardware, including without GPUs.Source: §3 · p. 5

4. Building LLM-based Proof Automation with Lean Copilot

Lean Copilot provides a framework for running LLM inference in Lean and building proof-automation tools. These tools suggest tactics, search for complete proofs, and select and annotate premises.

4. Building LLM-based Proof Automation with Lean Copilot

  • The framework supports three proof tasks and reusable interfaces for developers to build other tools or bring their own models.Its low-level interfaces support text-to-text generation and text-to-vector encoding.Source: §4 · pp. 5–6

4.1. Generating Tactic Suggestions

  • SUGGEST_TACTICS generates candidate tactics from current proof goals, simulates them, drops those that error, and displays the rest with their resulting goals.Candidates that finish the proof are colored green; others are blue.Source: §4.1 · p. 6

4.2. Searching for Complete Proofs

  • SEARCH_PROOF combines LLM-generated tactics with AESOP’s search, allowing the tactic rule set to vary with each goal rather than remain fixed.AESOP's fixed rule set can require problem-dependent configuration and cannot adaptively select tactics for intermediate goals.Source: §4.2 · p. 7

4.3. Selecting & Annotating Premises

  • Premise selection addresses cases where users lack a firm idea of which library premise to use, making keyword or library searches less reliable.Those searches can fail when a premise's formal name differs from what the user expects.Source: §4.3 · pp. 7–8
  • Premise selection ranks candidates by relevance to a proof goal using an encoded goal vector and precomputed premise embeddings.Selected premises are annotated as in scope or out of scope; the annotations provide type and docstring information or the needed module and definition code.Source: §4.3 · p. 8

5. Experiments

The experiments evaluate Lean Copilot’s tactic suggestion and proof-search tools on Mathematics in Lean, comparing them with AESOP in autonomous proving and human-assisted workflows. SEARCH_PROOF outperforms both comparison tools on reported measures of automation and human effort.

Experimental Setup

  • The study focuses on SUGGEST_TACTICS and SEARCH_PROOF because evaluating SELECT_PREMISES remains challenging without premise-selection ground truths.Source: §5 · p. 9
  • The human-assistance experiment enters ground-truth tactics one at a time and tests each tool on the remaining goals after each step.AESOP is used out of the box without manual rule-set configuration.Source: §5 · p. 9

Dataset and Experimental Setup

  • The evaluation covers all 168 tactic-style theorems in Mathematics in Lean, whose ground-truth proofs average 5.85 tactics.The book spans topics from sets and functions to topology, calculus, and measure theory.Source: §5 · p. 9

Results

  • 63.7% (107 out of 168) theorems were proved autonomously by SEARCH_PROOF, significantly more than by AESOP and SUGGEST_TACTICS.Source: §5 · p. 9
  • SEARCH_PROOF automates 74.2% of proof steps, versus 58.4% for SUGGEST_TACTICS and 40.1% for AESOP, and requires 2.08 manually entered tactics versus 3.11 and 3.86, respectively.The table caption identifies the comparison as covering SUGGEST_TACTICS, AESOP, and SEARCH_PROOF.Source: §5 · p. 10, Table 1 · p. 10

6. Conclusion

Lean Copilot runs LLM inference natively in Lean and provides tools for tactic suggestions, proof search, and premise selection. On Mathematics in Lean, its tools outperform AESOP on reported human-assistance and proof-step automation measures.

6. Conclusion

  • Lean Copilot is a framework for running LLM inference natively in Lean.Source: §6 · p. 10
  • Its tools generate tactic suggestions, search for proofs, and select premises, while general interfaces let users bring models or build additional tools.Source: §6 · p. 10
  • On Mathematics in Lean, Lean Copilot requires 2.08 manually entered proof steps on average versus 3.86 for AESOP, and automates 74.2% of proof steps versus AESOP’s 40.1%.The authors release code and artifacts and hope the tools will support more high-quality formal data and improve LLM capability in formal mathematics.Source: §6 · p. 10

Appendix A. Code & Artifacts

The authors make Lean Copilot’s code and artifacts available under a permissive MIT license and release evaluation code for transparency.

Appendix A. Code & Artifacts

  • Lean Copilot’s code and artifacts are open sourced under a permissive MIT license.Source: Appendix A · p. 18
  • The authors also release evaluation code for the experiments presented in Section 5 and Appendix C for full transparency.Source: Appendix A · p. 18

Appendix B. Generalizing Lean Copilot with Low-Level Interfaces

Appendix B broadens Lean Copilot beyond its three proof-automation tools with low-level text-generation and text-encoding interfaces. Developers can configure their own models and use server processes as an alternative to native inference.

Low-Level Interfaces

  • The two low-level interfaces let developers build proof-automation tools beyond the three included tasks: tactic suggestion, proof search, and premise selection.The interfaces are intended for advanced users and developers, rather than being immediate proof-automation tools themselves.Source: Appendix B · p. 18

Text-to-Text Generation

  • The text-to-text interface maps remaining goals to tactic suggestions for SUGGEST_TACTICS and SEARCH_PROOF, with beam search returning the top-k sequences.Users can bring a model, configure generation, and change fields such as the number of return sequences without declaring a new model.Source: Appendix B · pp. 18–19

Text-to-Vector Encoding

  • The text-to-vector interface encodes remaining goals and scores candidate premises using precomputed ReProver premise embeddings.Developers can bring their own encoder and encode any input sequence.Source: Figure 6 · p. 19, Appendix B · p. 20

Server Processes

  • Users can run generation and encoding through server processes, exposing APIs so Lean Copilot can use models hosted outside Lean.The paper gives examples including OpenAI GPT, Anthropic Claude, Google Gemini, and InternLM2.Source: Appendix B · p. 20

Appendix C. Detailed Experimental Results

Table 2 presents results for all Mathematics in Lean theorems with tactic-style proofs, including human-entered tactics and whether each tool completes a proof automatically. The evaluation materials support transparency, though neural-tool outcomes can vary between runs.

Appendix C. Detailed Experimental Results

  • The evaluation code is public, and theorem links lead to ground-truth proofs and corresponding exercise files.Problem files document experiment details, while solution files preserve the ground-truth proofs.Source: Appendix C · p. 20
  • A tool marker immediately after a proof means the automation did not help and users wrote all proof steps.The comments mark where SUGGEST_TACTICS, AESOP, or SEARCH_PROOF would automate the remainder.Source: Appendix C · p. 20
  • AESOP is reproducible because it is rule-based, whereas SUGGEST_TACTICS and SEARCH_PROOF are probabilistic and may generate different proofs on reruns.The experiment records the neural tools’ generated tactic or proof alongside the automation positions.Source: Appendix C · pp. 20–21
  • Table 2 covers all Mathematics in Lean theorems with tactic-based proofs, and its caption defines the tactic-count, human-tactic, and automatic-completion columns.The “Auto” value indicates whether a theorem is proved without human-entered tactics.Source: Appendix C · p. 20, Table 2 · p. 21

Appendix D. Impacts & Future Works

Lean Copilot is presented as an open-source framework for running LLM inference in Lean and supporting proof automation. The authors describe immediate uses and future directions, including connecting neural and symbolic work and adapting to growing projects.

LLM-Powered Proof Automation for Lean Users

  • Lean Copilot offers users tactic suggestions, proof completions, and premise selections to accelerate theorem proving in Lean.The authors report receiving community feedback about these tools.Source: Appendix D · p. 25

Building More Proof Automation

  • The framework can support additional proof-automation applications, including autoformalization, proof repair, proof search, progress prediction, and lifelong learning.The authors note efforts on proof progress prediction and lifelong learning.Source: Appendix D · p. 25

More Immediate Synchronization within the Field

  • Because Lean Copilot supports user-brought models, new neural models can be added to Lean, while AI developers can test models in the Lean environment.The authors describe the framework as a bridge between the neural and symbolic sides of the field.Source: Appendix D · pp. 25–26

Dynamic Copilots

Loading 2404.12534v3…