Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers

Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad

TL;DR

This work presents Lean-auto, a translation interface between Lean 4 and automated theorem provers (ATPs) that enables general-purpose proof automation for Lean 4. It introduces a novel monomorphization-based pipeline that first translates Lean 4 to dependent type theory, then to HOL*, and finally to HOL, with a universe lifting step to align with HOL semantics. A key contribution is the λ→* abstraction and saturating quantifier-instantiation framework, together with a robust handling of Lean 4 features such as dependent arguments, definitional equality, and extensive typeclass usage. Soundness of the main translation procedure is established, and experimental results on Mathlib4 show Lean-auto solves more problems than prior tools, highlighting its complementary role to existing tactics and hammers. This work thus advances practical ATP-based proof automation for Lean 4 and large formal libraries.

Abstract

Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose proof automation in ITPs such as Coq and Isabelle, leveraging the power of ATPs. An important component of a hammer is the translation algorithm from the ITP's logical system to the ATP's logical system. In this paper, we propose a novel translation algorithm for ITPs based on dependent type theory. The algorithm is implemented in Lean 4 under the name Lean-auto. When combined with ATPs, Lean-auto provides general-purpose, ATP-based proof automation in Lean 4 for the first time. Soundness of the main translation procedure is guaranteed, and experimental results suggest that our algorithm is sufficiently complete to automate the proof of many problems that arise in practical uses of Lean 4. We also find that Lean-auto solves more problems than existing tools on Lean 4's math library Mathlib4.

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers

TL;DR

This work presents Lean-auto, a translation interface between Lean 4 and automated theorem provers (ATPs) that enables general-purpose proof automation for Lean 4. It introduces a novel monomorphization-based pipeline that first translates Lean 4 to dependent type theory, then to HOL*, and finally to HOL, with a universe lifting step to align with HOL semantics. A key contribution is the λ→* abstraction and saturating quantifier-instantiation framework, together with a robust handling of Lean 4 features such as dependent arguments, definitional equality, and extensive typeclass usage. Soundness of the main translation procedure is established, and experimental results on Mathlib4 show Lean-auto solves more problems than prior tools, highlighting its complementary role to existing tactics and hammers. This work thus advances practical ATP-based proof automation for Lean 4 and large formal libraries.

Abstract

Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose proof automation in ITPs such as Coq and Isabelle, leveraging the power of ATPs. An important component of a hammer is the translation algorithm from the ITP's logical system to the ATP's logical system. In this paper, we propose a novel translation algorithm for ITPs based on dependent type theory. The algorithm is implemented in Lean 4 under the name Lean-auto. When combined with ATPs, Lean-auto provides general-purpose, ATP-based proof automation in Lean 4 for the first time. Soundness of the main translation procedure is guaranteed, and experimental results suggest that our algorithm is sufficiently complete to automate the proof of many problems that arise in practical uses of Lean 4. We also find that Lean-auto solves more problems than existing tools on Lean 4's math library Mathlib4.

Paper Structure

This paper contains 32 sections, 8 theorems, 31 equations, 6 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Dependent Type Theory
  5. Logical Systems of ITPs and ATPs
  6. Pure Type Systems $\lambda C, \lambda_\to, \lambda_\to^*$ and Related Logical Systems
  7. Lean and Mathlib
  8. Encoding-based Translation and Monomorphization
  9. An Overview of Lean-auto
  10. $\lambda_\to^*$ Abstraction
  11. Quantifier Instantiation
  12. Challenges Related to Dependent Type Theory and Lean 4
  13. Dependent Arguments are Dynamic:
  14. $\text{HOL}^*$ Instances are Dynamic:
  15. Definitional Equality:
  16. ...and 17 more sections

Key Result

theorem thmcountertheorem

For all $t \in \mathcal{T}_\to$, $\rho_\ell^*(\rho_\ell(t)) = t$.

Figures (6)

  • Figure 1: Translation workflow of Lean-auto.
  • Figure 2: Lean 4 proof state of a problem involving List.
  • Figure 3: Lean 4 proof state after variable introduction and application of proof by contradiction, with implicit arguments displayed. Note that the equality sign in Figure \ref{['leanlistpretty']} is syntactic sugar for the polymorphic function Eq shown here.
  • Figure 4: The function DFunLike.coe from MathLib4 and an expression containing it.
  • Figure 5: Comparison with existing tools. Our benchmark set contains 149135 problems.
  • ...and 1 more figures

Theorems & Definitions (31)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • theorem thmcountertheorem
  • proof
  • theorem thmcountertheorem
  • ...and 21 more