Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

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

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Lean-auto presents a sound translation from Lean 4's dependent type theory to higher-order logic, giving Lean 4 its first general-purpose ATP-based hammer, and reports solving 36.6% of Mathlib4 theorems with the Duper backend.

desk verdict Genuine first ATP hammer for Lean 4 with a clean core translation and large honest benchmark, but the soundness and completeness claims need qualification. read the letter →

arxiv 2505.14929 v2 pith:DRJTWQFE submitted 2025-05-20 cs.LO

Yicheng Qian , Joshua Clune , Clark Barrett , Jeremy Avigad This is my paper · ORCID
classification cs.LO MSC 03B3568V1568V20
keywords Lean4automatedtheoremprovinghammermonomorphizationdependenttypetheoryhigher-orderlogicMathlib4proofautomation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Lean-auto's aim is to give Lean 4 the kind of general-purpose, ATP-powered proof search that hammers provide for other interactive provers. The paper's central contribution is a translation procedure from Lean 4's dependent type theory to monomorphic higher-order logic, carried out by preprocessing followed by quantifier instantiation, abstraction into a multi-universe simply typed lambda calculus, and universe lifting. The main translation is proven sound, and for the native Duper backend the resulting proofs are checked by the Lean 4 kernel. On 149,142 user-declared Mathlib4 theorems, fed the premises used in the human proofs, Lean-auto with Duper solves 36.6%, which is 5.0 percentage points more than the previous best existing tool, Aesop; the virtual best of Lean-auto's backends reaches 41.5%. The evaluation deliberately omits premise selection and full proof reconstruction, so the measured numbers reflect the translation's capability rather than a complete hammer.

What carries the argument

The engine is a four-stage pipeline: preprocessing (reduction, inductive-type handling, quantifier introduction, and proof by contradiction), followed by the three monomorphization steps of quantifier instantiation, $\lambda^\ast_\to$ abstraction, and universe lifting. Quantifier instantiation runs a saturation loop in which $\mathrm{HOL}^\ast$ instances, meaning polymorphic constants with their dependent arguments instantiated, are matched against hypothesis instances to produce new ones until closure or a threshold. The $\lambda^\ast_\to$ abstraction step then replaces each $\mathrm{HOL}^\ast$ instance by a fresh variable, so the translated problem lives in simply typed $\lambda$ calculus with many universe levels; its correctness rests on the definition of essentially higher-order provable problems and the theorem that such problems are provable in $\lambda\mathrm{C}$. The quasi-monomorphic predicate $\mathrm{QMono}$ defines exactly which terms the abstraction accepts: proofs are never bound by $\lambda$ or a dependent $\forall$, dependently typed free variables have no bound variables in their dependent arguments, and dependently typed bound variables are never applied to dependent arguments. This predicate is what makes the soundness argument go through, and it is also where the translation's incompleteness concentrates.

What would settle it

Run Lean-auto on a benchmark of goals whose human proofs require a bound function to be applied to a dependent argument involving a proof, for example $\forall (f : \forall x, P\,x \to Q\,x)$ followed by applying $f$ to a proof of $P\,a$; if the solve rate on such problems falls far below 36.6%, the quasi-monomorphic restriction is the practical bottleneck.

Watch

Extended reading notes

Core claim

On its own terms, the paper's discovery is that the gap between Lean 4's dependent type theory and the higher-order logic used by ATPs can be bridged by a three-stage monomorphization. Instead of encoding typing judgements as uninterpreted predicates, as CoqHammer does, Lean-auto instantiates polymorphic constants to the specific instances occurring in the goal, searches for further instances with a saturation loop that matches hypotheses against each other, abstracts the resulting quasi-monomorphic terms into a simply typed $\lambda$ calculus with multiple universe levels, and then erases universe levels. The paper proves that if a $\lambda\mathrm{C}$ problem is essentially higher-order provable, meaning it is the image of a provable $\mathrm{HOL}^\ast$ problem under a substitution, then it is provable in $\lambda\mathrm{C}$, which is what makes the translation sound. Experimentally, the Duper backend with kernel-checked reconstruction proves 54,570 of the 149,142 Mathlib4 theorems, or 36.6%, and the virtual best of all Lean-auto backends proves 61,906, or 41.5%.

Load-bearing premise

The load-bearing assumption is that after quantifier instantiation, most real Lean 4 goals are quasi-monomorphic: proofs are never bound by functions or dependent universal quantifiers, and bound variables are never applied to dependent arguments. If many practical goals violate that shape, Lean-auto cannot translate them, and the measured 36.6% solve rate is an upper bound rather than a general automation rate.

Editorial extensions

If this is right

  • Lean 4 users can hand a goal and its premises to Lean-auto and dispatch goals that previously required manual rewrite chains, at least within the 10-second budget used in evaluation.
  • For the Duper backend, every successful run returns a proof that is checked by the Lean 4 kernel, so the automation is not just an unchecked oracle.
  • Because the translation is sound, later improvements in premise selection or backend speed should raise the solve rate without weakening the guarantee.
  • The combined virtual best of 53.2% shows ATP-based search and existing rule-based tactics solve largely complementary sets of problems.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: The same $\lambda\mathrm{C}$-to-$\mathrm{HOL}^\ast$ monomorphization, once preprocessed, could in principle be reused for other dependently typed provers with similar typeclass and universe features.
  • Editorial inference: A direct stress test of the quasi-monomorphic restriction—goals that bind proofs or instantiate dependent arguments of bound variables—would show how far the 36.6% rate degrades outside Mathlib4's typical theorem shapes.
  • Editorial inference: Re-running the benchmark with genuine premise selection instead of the human proofs' premises would reveal how much of the reported gain survives when premises are not idealized.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. This paper presents Lean-auto, a translation pipeline from Lean 4's dependent type theory to monomorphic HOL, consisting of preprocessing, quantifier instantiation, λ*-abstraction, and universe lifting. The paper defines quasi-monomorphic (QMono) terms, proves a soundness theorem (Appendix F, Theorem 8) stating that an 'essentially higher-order' problem that is provable after λ*-abstraction is provable in λC, and implements the pipeline as a Lean 4 tactic that can invoke Duper, Zipperposition, Z3, and CVC5. On 149,142 Mathlib4 user-declared theorems with premises taken from the human proofs, Lean-auto+Duper solves 36.6% of the problems, 5.0 percentage points more than Aesop, and the overall virtual best solver solves 53.2%. The paper positions Lean-auto as the first ATP-based hammer-style automation for Lean 4.

Significance. If the results hold, this is the first ATP-based hammer for Lean 4 and a useful design for translating dependent type theory into HOL. The formal EHOP soundness theorem (Appendix F, Theorem 8) is a real theoretical contribution, as is the kernel-checked proof reconstruction for Duper; the artifact is reusable and the benchmark methodology in Appendix L is carefully documented. The measured solve counts are based on a fixed Mathlib4 commit, oracle premises, and a 10-second limit, and the comparison with Aesop and simp_all is conducted under the same premise supply. The paper's main weakness is that the translation's coverage is unmeasured: QMono rejection, maxInsts truncation, and the 17% failure rate reported in Appendix I could mean that the headline solve rate is an upper bound, so the 'sufficiently complete' claim in the abstract goes beyond the evidence. With this coverage data supplied and the soundness statement qualified by backend, the paper would be a strong CAV contribution.

major comments (3)
  1. [§6, Algorithm 1; Appendix G, Definition 18; Appendix I] The QMono filter is never measured, so the headline 36.6% solve rate may be an upper bound. The saturation loop in Algorithm 1 returns only the hypothesis instances that satisfy QMono(Γ;∅,h); Definition 18(4) rejects dependent ∀-binders whose domain is Prop (e.g., statements of the form ∀ {n} (h : n ≠ 0), body(h), which arise from casts, Fin, Subtype, and equality elimination), and Definition 18(2) rejects free variables whose dependent arguments contain bound variables. The paper's own Appendix I reports 88 monomorphization failures out of 512 sampled theorems (17.2%), but it does not decompose those failures into non-QMono rejections versus timeouts or other errors, and the full evaluation never reports how many of the 149,142 benchmark problems have empty or truncated monohi. If a substantial fraction of the 63.4% unsolved problems are non-QMono, then 36.6% is an upper bound on what the translation can deliver even with oracle premises, and the abstract's claim that the algorithm is 'sufficiently complete to automate the proof of many problems that arise in practical uses of Lean 4' is not established. Please add a coverage table: for each benchmark problem, report whether monohi is empty, nonempty but truncated by maxInsts, or complete, and give solve rates conditioned on those classes.
  2. [§1; §8; Appendix F, Theorem 8] The soundness guarantee is not uniform across the evaluated backends. The abstract states 'Soundness of the main translation procedure is guaranteed,' but Section 1 explicitly says that only native provers (Duper) have kernel-checked proof reconstruction, while Z3, CVC5, and Zipperposition solutions are marked 'solved' with a warning that the ATP output is trusted. Theorem 8 in Appendix F establishes soundness of the EHOP/HOL* abstraction step in isolation; it does not make the full solver chain sound for the non-Duper backends. Please separate 'soundly reconstructed solves' from 'trusted solver calls' in the results table and in the abstract, and reserve the word 'sound' for the pipeline whose output is kernel-checked.
  3. [§8; Abstract] The headline comparison 'Lean-auto solves more problems than existing tools on Mathlib4' should be labeled as an oracle-premise comparison. The evaluation sends to every premise-accepting tool the exact premises used in the human proof of each theorem, which the paper itself describes as emulating an ideal premise selection algorithm. This measures translation quality under a perfect premise selector, not an end-to-end hammer, yet the abstract states the comparison without this qualification. Please qualify the headline with 'given oracle premises from the human proofs' and state that premise selection is left to future work.
minor comments (5)
  1. [Figure 5 and §8] Figure 5's caption says the benchmark set contains 149,135 problems, while the text in §8 and the abstract-adjacent discussion say 149,142; please align these numbers.
  2. [Algorithm 1 (and Algorithm 4)] The pseudocode sets `hi := H` and then, for each h in H, executes `hi.push((0,h))`; since hi is described as a list of λC terms, the pair type `(0,h)` needs a consistent type annotation or the initialization should be changed.
  3. [Introduction] There is a typo in the first paragraph of the Introduction: 'Challanges' should be 'Challenges'.
  4. [Appendix L, Experimental Setup 2] Step 2(e)(ii) says to 'create the syntax S that invokes tac' but does not give a concrete example of that syntax for a premise-accepting tactic; one concrete invocation would make the setup reproducible without reading the artifact.
  5. [Appendix G, Definition 18(4)] The condition `¬F V(s)∩B=∅` is ambiguous as printed; it should be parenthesized to make clear whether it means `¬(FV(s) ∩ B = ∅)` or `¬FV(s) ∩ B = ∅`.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: soundness is proved by independent substitution/embedding theorems, and the empirical claims are measured against external Mathlib4 theorems rather than fitted to the translation's own definitions.

full rationale

The central derivation chain is self-contained. Soundness of λ*-abstraction and universe lifting is established by formal theorems (Theorem 8 via substitution Theorem 6; Theorems 1–4 for HOL*/HOL equivalence; Theorem 5 via GLift), none of which assume the target result. The EHOP/Theorem 8 step is a standard soundness-preservation argument, not a definitional equivalence: it shows that a provable HOL* problem plus a substitution yields a provable λC problem. The experimental claims are external: 149,142 Mathlib4 theorems with premises taken from human proofs, compared against rfl, simp_all, and Aesop; no parameter was fitted to make the 36.6% solve rate true. The only same-group dependency is Duper as the native backend, but it is not load-bearing for the paper's central soundness claim, since Lean-auto reconstructs and kernel-checks native proofs, and translation soundness is argued separately. The QMono filter (Definition 18) and Appendix I's 88/512 monomorphization failures are genuine completeness limitations, and the 36.6% solve rate is an upper bound under oracle premises, but that is a scope caveat, not circularity.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

No new physical or mathematical entities are postulated. HOL* is a formal intermediate logic defined in the paper, not an entity with independent empirical content. The free parameters are resource and configuration knobs, not fitted constants, and the axioms are the explicit or implicit domain assumptions on which the translation and evaluation rest.

free parameters (3)
  • maxInsts
    Saturation loop cutoff in quantifier instantiation (Algorithms 1 and 4); chosen as a resource threshold, not fitted to data, but it bounds completeness.
  • maxHeartbeats = 65536 heartbeats
    Resource limit for native Lean tools, matched to roughly 10 seconds in Sect. 8; a hand-set evaluation parameter.
  • definitional equality and unfolding instructions
    Users can supply d[...] and u[...] instructions in preprocessing (Sect. 7); these control how much definitional equality is made explicit and affect translation success.
assumptions (4)
  • domain assumption The monomorphization assumption: many practical proofs in dependent type theory can be carried out in monomorphic HOL after instantiating polymorphic constants.
    Stated in Sect. 3; this is the core completeness limitation and is not proved for all Lean goals.
  • domain assumption The QMono predicate exactly characterizes terms that lambda-star abstraction can translate (Appendix G, Definition 18).
    Algorithm 2 only handles QMono terms; the empirical usefulness of Lean-auto depends on the fraction of Mathlib4 goals satisfying this condition.
  • domain assumption Lean 4's classical axioms (excluded middle, choice, function extensionality) are available and used during proof reconstruction.
    Sect. 2.4 states classical axioms are built into Lean 4 and Lean-auto uses them; this is an assumption about the ambient logic.
  • domain assumption External ATP outputs from Z3, CVC5, and Zipperposition are correct when no proof reconstruction is performed.
    Sect. 1: for these backends Lean-auto trusts the ATP output and only warns; soundness of the end-to-end tool depends on solver correctness.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Lean-auto: An Interface between Lean 4 and Automated Theorem Provers." pith.science (2026). https://pith.science/paper/DRJTWQFE

@misc{pith2026250514929,
  author       = {Pith},
  title        = {Pith review of: Lean-auto: An Interface between Lean 4 and Automated Theorem Provers},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DRJTWQFE}},
  note         = {Machine review of arXiv:2505.14929}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2505.14929 by the authors.

Figure 1
Figure 1. Translation workflow of Lean-auto. In our paper, we work backwards in Lean-auto’s translation workflow. We start from λ ∗ → abstraction (Sect. 5), then quantifier instantiation (Sect. 6), and end with preprocessing (Sect. 7). This is because it is easier to be￾gin with the simpler logical system and progressively take into account more features of the highly expressive Lean 4 language. We leave universe lifting to A… view at source ↗
Figure 2
Figure 2. Lean 4 proof state of a problem involving List. The Lean 4 proof state of the problem we will consider is shown in [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Lean 4 proof state after variable introduction and application of proof by con￾tradiction, with implicit arguments displayed. Note that the equality sign in [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: The function DFunLike.coe from MathLib4 and an expression containing it. Dependent Arguments are Dynamic: In λC, whether an argument is de￾pendent depends on how previous arguments are instantiated. Consider the example shown in [PITH_FULL_IMAGE:figures/full_fig_p012_4.png]
Figure 5
Figure 5. Figure 5: Comparison with existing tools. Our benchmark set contains 149135 problems [PITH_FULL_IMAGE:figures/full_fig_p019_5.png]
Figure 6
Figure 6. Figure 6: #Solved - Cumulative Time plot (left) and #Solved - Time plot (right) [PITH_FULL_IMAGE:figures/full_fig_p019_6.png]
Figure 7
Figure 7. Figure 7: Result of experiment on translation The result is presented in [PITH_FULL_IMAGE:figures/full_fig_p037_7.png]
Figure 8
Figure 8. Figure 8: Result of experiment on reducing input expressions The result is presented in [PITH_FULL_IMAGE:figures/full_fig_p038_8.png]
Figure 9
Figure 9. Figure 9: Comparison of Duper with and without Lean-auto. We see that when Duper is used without Lean-auto, it only solves 8.2% of the problems, and it is slower on solved problems compared to “Duper with Lean-auto”. Duper also exhibits unexpected behaviors during the experiment…
Figure 10
Figure 10. Figure 10: Experimental Setup 1 However, Experimental Setup 1 is unfair because it favors simp_all and aesop. This is related to the fact that these two tactics have access to theorems tagged with the “simp” attribute. Suppose a theorem T in Mathlib4 is tagged with “simp”. If we…
Figure 11
Figure 11. Figure 11: We employ a per-file evaluation scheme for better efficiency. To run a tactic tac on a Mathlib4 file F: 1. Retrieve the content of F 2. For each command C in F: (a) Record the environment E before executing C. E contains all the constants declared by commands prior to…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

    cs.LO 2026-02 conditional novelty 7.0 of 10

    A finite set of atomic Lean tactics plus a transposing atomization algorithm lets a small graph neural network, Nazrin, be trained on converted proofs and prove held-out formal theorems.

Reference graph

Works this paper leans on

64 extracted references · 49 canonical work pages · cited by 1 Pith paper

  1. [1]

    Avigad, J., de Moura, L., Kong, S., Ullrich, S.: Theorem Proving in Lean4 (2025), https://leanprover.github.io/theorem_proving_in_lean4

    work page 2025

  2. [2]

    In: Fisman, D., Rosu, G

    Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for Lean-auto: An Interface between Lean 4 and A...

    2022

  3. [3]

    Barendregt, H.P.: Lambda calculi with types, pp. 117–309. Oxford University Press, Inc., USA (1993),https://dl.acm.org/doi/10.5555/162552.162561

    work page arXiv 1993

  4. [4]

    Barras, B., Boutin, S., Cornes, C., Courant, J., Filliâtre, J.C., Giménez, E., Her- belin, H., Huet, G.P., Muñoz, C.A., Murthy, C.R., Parent, C., Paulin-Mohring, C., Saïbi, A., Werner, B.: The Coq proof assistant : reference manual, version 6.1 (1997),https://api.semanticscholar.org/CorpusID:54117279

    work page 1997

  5. [5]

    In: Benzmüller, C., Heule, M.J., Schmidt, R.A

    Bhayat, A., Suda, M.: A higher-order Vampire (short paper). In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds.) Automated Reasoning. pp. 75–85. Springer Na- ture Switzerland, Cham (2024).https://doi.org/10.1007/978-3-031-63498-7_ 5

    work page doi:10.1007/978-3-031-63498-7_ 2024

  6. [6]

    Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason.9, 101–148 (2016),https://api.semanticscholar. org/CorpusID:218028818

    work page 2016

  7. [7]

    Böhme, S.: Proving Theorems of Higher-Order Logic with SMT Solvers. Ph.D. the- sis, Technical University Munich (2012),https://nbn-resolving.org/urn:nbn: de:bvb:91-diss-20120511-1084525-1-4

    work page 2012

  8. [8]

    In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M

    Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda – a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. pp. 73–78. Springer Berlin Heidelberg, Berlin, Heidelberg (2009).https://doi.org/10.1007/978-3-642-03359-9_6

    doi:10.1007/978-3-642-03359-9_6 2009

Show all 64 references
  1. [9]

    In: Naumowicz, A., Thiemann, R

    Carneiro, M., Brown, C.E., Urban, J.: Automated theorem proving for Metamath. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interac- tive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs),vol.268,pp.9:1–9:19.Schloss...

    2023 doi

  2. [10]

    In: International Confer- enceonInteractiveTheoremProving(2024),https://api.semanticscholar.org/ CorpusID:272330518

    Clune, J., Qian, Y., Bentkamp, A., Avigad, J.: Duper: A proof-producing su- perposition theorem prover for dependent type theory. In: International Confer- enceonInteractiveTheoremProving(2024),https://api.semanticscholar.org/ CorpusID:272330518

    2024

  3. [11]

    Information and Computa- tion76(2), 95–120 (1988).https://doi.org/10.1016/0890-5401(88)90005-3

    Coquand, T., Huet, G.: The calculus of constructions. Information and Computa- tion76(2), 95–120 (1988).https://doi.org/10.1016/0890-5401(88)90005-3

    1988 doi

  4. [12]

    In: Martin-Löf, P., Mints, G

    Coquand, T., Paulin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG-88. pp. 50–66. Springer Berlin Heidelberg, Berlin, Heidelberg (1990).https://doi.org/10.1007/3-540-52335-9_47

    1990 doi

  5. [13]

    Journal of Automated Reasoning61, 423 – 453 (2018),https://api

    Czajka, L., Kaliszyk, C.: Hammer for Coq: Automation for dependent type theory. Journal of Automated Reasoning61, 423 – 453 (2018),https://api. semanticscholar.org/CorpusID:11060917

    2018

  6. [14]

    In: TOPL (1994),https://api.semanticscholar.org/CorpusID:9227770

    Hall, C.V., Hammond, K., Jones, S.L.P., Wadler, P.: Type classes in Haskell. In: TOPL (1994),https://api.semanticscholar.org/CorpusID:9227770

    1994

  7. [15]

    In: McRobbie, M.A., Slaney, J.K

    Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction — Cade-13. pp. 313–327. Springer Berlin Heidelberg, Berlin, Heidelberg (1996).https://doi.org/10.1007/ 3-540-61511-3_97

    1996

  8. [16]

    In: Computational Logic (2014),https://api.semanticscholar.org/CorpusID: 30345151

    Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Computational Logic (2014),https://api.semanticscholar.org/CorpusID: 30345151

    2014

  9. [17]

    De- sign and Application of Strategies/Tactics in Higher Order Logics, number 22 Y

    Hurd, J.: First-order proof tactics in higher-order logic theorem provers. De- sign and Application of Strategies/Tactics in Higher Order Logics, number 22 Y. Qian et al. NASA/CP-2003-212448 in NASA Technical Reports pp. 56–68 (2003),https: //api.semanticscholar.org/CorpusID:11201048

    2003

  10. [18]

    Math- ematics in Computer Science9(1), 5–22 (Mar 2015).https://doi.org/10.1007/ s11786-014-0182-0

    Kaliszyk, C., Urban, J.: Hol(y)hammer: Online ATP service for HOL light. Math- ematics in Computer Science9(1), 5–22 (Mar 2015).https://doi.org/10.1007/ s11786-014-0182-0

    2015

  11. [19]

    Journal of Automated Reasoning 55(3), 245–256 (Oct 2015).https://doi.org/10.1007/s10817-015-9330-8

    Kaliszyk, C., Urban, J.: Mizar 40 for mizar 40. Journal of Automated Reasoning 55(3), 245–256 (Oct 2015).https://doi.org/10.1007/s10817-015-9330-8

    2015 doi

  12. [20]

    In: Sharygina, N., Veith, H

    Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. pp. 1–35. Springer Berlin Heidel- berg, Berlin, Heidelberg (2013).https://doi.org/10.1007/978-3-642-39799-8_ 1

    2013 doi

  13. [21]

    In: Proceedingsofthe12thACMSIGPLANInternationalConferenceonCertifiedPro- grams and Proofs

    Limperg, J., From, A.H.: Aesop: White-box best-first proof search for Lean. In: Proceedingsofthe12thACMSIGPLANInternationalConferenceonCertifiedPro- grams and Proofs. pp. 253–266. CPP 2023, Association for Computing Machinery, New York, NY, USA (2023).https://doi.org/10.1145/3...

    2023

  14. [22]

    Mikuła, M., Tworkowski, S., Antoniak, S., Piotrowski, B., Jiang, A.Q., Zhou, J.P., Szegedy, C., Kuciński, Ł., Miłoś, P., Wu, Y.: Magnushammer: A transformer-based approachtopremiseselection.ArXiv(2024),https://arxiv.org/abs/2303.04488

    2024 arXiv

  15. [23]

    In: Ramakrishnan, C.R., Rehof, J

    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    2008 doi

  16. [24]

    In: CADE (2021),https://api.semanticscholar.org/CorpusID: 235800962

    de Moura, L.M., Ullrich, S.: The Lean 4 theorem prover and program- ming language. In: CADE (2021),https://api.semanticscholar.org/CorpusID: 235800962

    2021

  17. [25]

    Paulson,L.C.:AgenerictableauproveranditsintegrationwithIsabelle.J.Univers. Comput. Sci.5, 73–87 (1999),https://api.semanticscholar.org/CorpusID: 2551237

    1999

  18. [26]

    In: IWIL@LPAR (2012),https://api.semanticscholar.org/CorpusID:598752

    Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL@LPAR (2012),https://api.semanticscholar.org/CorpusID:598752

    2012

  19. [27]

    ArXivabs/2009.03393(2020),https://api.semanticscholar.org/ CorpusID:221535103

    Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. ArXivabs/2009.03393(2020),https://api.semanticscholar.org/ CorpusID:221535103

    2020 arXiv

  20. [28]

    Qian, Y., Clune, J., Barrett, C., Avigad, J.: Lean-auto: An interface between lean 4 and automated theorem provers (2025),https://arxiv.org/abs/2505.14929

    2025 arXiv

  21. [29]

    Experimental Mathematics31(2), 349–354 (2022).https://doi.org/10.1080/10586458.2021.1926016

    Scholze, P.: Liquid tensor experiment. Experimental Mathematics31(2), 349–354 (2022).https://doi.org/10.1080/10586458.2021.1926016

    2022

  22. [30]

    AI Commun.15, 111–126 (2002),https: //api.semanticscholar.org/CorpusID:884116

    Schulz, S.: E - a brainiac theorem prover. AI Commun.15, 111–126 (2002),https: //api.semanticscholar.org/CorpusID:884116

    2002

  23. [31]

    In: Klein, G., Gam- boa, R

    Sozeau, M., Tabareau, N.: Universe polymorphism in Coq. In: Klein, G., Gam- boa, R. (eds.) Interactive Theorem Proving. pp. 499–514. Springer International Publishing, Cham (2014).https://doi.org/10.1007/978-3-319-08970-6_32

    2014 doi

  24. [32]

    In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

    The Mathlib Community: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 367–381. CPP 2020, Association for Computing Machinery, New York, NY, USA (2020).https://doi.org/10.1145/3372885.3373824

    2020

  25. [33]

    Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. J. Autom. Reason.66(4), 541–564 (Nov 2022).https://doi.org/10.1007/s10817-021-09613-z Lean-auto: An Interface between Lean 4 and Automated Theorem Provers 23

    2022 doi

  26. [34]

    In: International Conference on Tools and Algorithms for Construction and Analysis of Systems (2023),https://api.semanticscholar

    Vukmirović, P., Blanchette, J.C., Schulz, S.: Extending a high-performance prover to higher-order logic. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems (2023),https://api.semanticscholar. org/CorpusID:249226027

    2023

  27. [35]

    In: International Conference on Theorem Proving in Higher Order Logics (2008),https://api

    Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: International Conference on Theorem Proving in Higher Order Logics (2008),https://api. semanticscholar.org/CorpusID:13752195

    2008

  28. [36]

    ArXivabs/1905.09381(2019),https://api.semanticscholar.org/ CorpusID:162184110

    Yang, K., Deng, J.: Learning to prove theorems via interacting with proof as- sistants. ArXivabs/1905.09381(2019),https://api.semanticscholar.org/ CorpusID:162184110

    2019 arXiv

  29. [37]

    ArXivabs/2306.15626(2023),https://api.semanticscholar

    Yang, K., Swope, A.M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R.J., Anandkumar, A.: Leandojo: Theorem proving with retrieval-augmented lan- guage models. ArXivabs/2306.15626(2023),https://api.semanticscholar. org/CorpusID:259262077 A Logical Symbols ofλC ...

    2023 arXiv

  30. [38]

    :=U ′ ℓ ρ(x) :=x,forx∈V ρ(M N) :=ρ(M)ρ(N)ρ(λ(x:s).M) :=λ(x:ρ(s)).ρ(M) ρ(⊥′) :=⊥ ′ ρ(→′) :=→′ ρ(∀′ s) :=∀ ′ ρ(s) ρis extended to contexts as follows:ρ(∅) :=∅;ρ(Γ, x:σ) :=ρ(Γ), x:ρ(σ) Theorem 1.For allt∈ T→,ρ ∗ ℓ (ρℓ(t)) =t. Proof. Induction on the construction rules ofT→. Theor...

  31. [39]

    Ifs=a, wherea∈Vis a variable, then we can define Upa :=GLift.up ℓ′,ℓ aDown a :=Glift.down ℓ′,ℓ a

  32. [40]

    Ifs= (α→β)and the induction hypothesis holds forαandβ, then we can define Upα→β :=λ(f:α→β) (x:UpTypeα).Up β (f(Down α x)) Downα→β :=λ(f:UpTypeα→UpTypeβ) (x:α).Down β (f(Up α x)) The rationale ofUpType(α→β) :=UpTypeα→UpTypeβis that, given f xin the canonical embedding of HOL∗, ...

  33. [41]

    Ifxis not a free variable, then we definex′ asx ′ :=Up s xin Lean 4

    Ifxis a variable andx:s, thenULiftTrans(x) :=x ′. Ifxis not a free variable, then we definex′ asx ′ :=Up s xin Lean 4. Ifxis a bound variable, no further operation is needed. 2.ULiftTrans(f x) :=ULiftTrans(f)ULiftTrans(x) 3.ULiftTrans(λ(x:s). y) :=λ(x ′ :UpTypes).ULiftTrans(y)...

  34. [42]

    There exists aλCtermssuch thatΓ ′ ⊢ σ(t1) :sandΓ ′ ⊢ σ(t2) :s

  35. [43]

    σ(t1) ∼= σ(t2)(i.e., σ(t1)and σ(t2)areβη-equivalent)

  36. [44]

    tis a quasi-monomorphic term under contextΓ, with variables inBbeing bound variables

    For all variablesv∈Γ\M,σ(v) =v. Then(Γ, Γ ′, σ)is called aM-unifier oft 1 andt 2. In the context of Lean, this corresponds to a unifier oft 1 andt 2 under contextΓ, withMas the set of metavariables. Definition 13.The canonical embeddingπ ∗ :T ∗ → → TC of HOL∗ intoλCis defined ...

  37. [45]

    , tn, QMono(Γ;B, x t1

    For variablex∈Band termst 1, . . . , tn, QMono(Γ;B, x t1 . . . tn) :=DArgs(Γ;x,(t 1 . . . tn)) =∅∧ ∀i∈ {1, . . . , n}.QMono(Γ;B, ti)

  38. [46]

    , tn, QMono(Γ;B, x t1

    For variablex /∈Band termst 1, . . . , tn, QMono(Γ;B, x t1 . . . tn) := (∀t∈DArgs(Γ;x,(t 1, . . . , tn)).F V(t)∩B=∅)∧ (∀t∈LArgs(Γ;x,(t 1, . . . , tn)).QMono(Γ;B, t))

  39. [47]

    Qian et al

    For variablexand termss, t QMono(Γ;B, λ(x:s).t) :=F V(s)∩B=∅ ∧(Γ̸⊢s:U 0) ∧QMono(Γ, x:s;B∪ {x}, t) 32 Y. Qian et al

  40. [48]

    For variablexand termss, tsuch thatx∈F V(t), QMono(Γ;B,∀(x:s).t) :=¬F V(s)∩B=∅ ∧(Γ̸⊢s:U 0)∧(Γ⊢t:U 0)∧ QMono(Γ, x:s;B∪ {x}, t)

  41. [49]

    For termss, t, QMono(Γ;B, s→t) := (Γ⊢s:U 0)∧(Γ⊢t:U 0)∧ QMono(Γ;B, s)∧QMono(Γ;B, t) According to the definition ofQMono, terms coming from canonical embedding of HOL∗ terms are automatically quasi-monomorphic, e.g. QMono(α:U 1, p: (α→α)→U 0;∅,∀(p:α→α).f p) Proofs are not allowe...

  42. [50]

    For a termt, iftis inH, thengetL VarName(t)returns the HOL∗ free variable corresponding tot, otherwise it creates a new HOL∗ free variable fort

  43. [51]

    tn wherewis not an application,getAppFn(t) = w,getAppArgs(t) = (t 1,

    For a termt=w t 1 . . . tn wherewis not an application,getAppFn(t) = w,getAppArgs(t) = (t 1, . . . , tn)

  44. [52]

    , tn,mkAppN(w,(t 1,

    For termsw, t1, . . . , tn,mkAppN(w,(t 1, . . . , tn)) =w t1 . . . tn

  45. [53]

    substitution

    For a contextΓand a termt,inferType(Γ, t)computes theβ-normal form of the type oftunderΓ. Note thatlamAbstonly returns the HOL ∗ problem (as a HOL∗ term). The “substitution” from HOL∗ toλCneeds to be obtained by computing the inverse ofHafter the execution of the algorithm. Al...

  46. [54]

    (xm : sm).t t1

    A constant instance oftis aλCterm of the formλ(x 1 :s 1). . .(xm : sm).t t1 . . . tk that is type correct underΓ, wheres 1, . . . , sm, t1, . . . tk are λCterms

  47. [55]

    (xn :r n).b, a hypothesis instance oftis aλCterm of the form∀(y 1 :s 1)

    Fort=∀(x 1 :r 1). . .(xn :r n).b, a hypothesis instance oftis aλCterm of the form∀(y 1 :s 1). . .(ym :s m).b[t1/x1]. . .[tn/xn], wheres 1, . . . , sm, t1, . . . , tn areλCterms, andt 1[t2/x]stands for the term obtained by replacing all the xint 1 witht 2. Unless otherwise stat...

  48. [56]

    , tn, holInsts(Γ;B, x t1

    For variablexand termst 1, . . . , tn, holInsts(Γ;B, x t1 . . . tn) := ( S∪ {l}, F V(l)∩B=∅ S,otherwise where l:=LFun(Γ;x,(t 1 . . . tn))S:= [ t∈LArgs(Γ;x,(t 1,...,tn)) holInsts(Γ;V, t)

  49. [57]

    For variablexand termsa, b, holInsts(Γ;B,∀(x:a).b) =holInsts(Γ;B, λ(x:a).b) :=holInsts(Γ;B, a)∪holInsts(Γ, x:a;B∪ {x}, b)

  50. [58]

    The matching procedure in the saturation loop is handled bymatchInstand match

    Otherwise,holInsts(Γ;B, t) :=∅. The matching procedure in the saturation loop is handled bymatchInstand match

  51. [59]

    The pseu- docode formatchis given in Algorithm 3

    Given contextΓ, variable setMand termsm, h,match(Γ;M, m, h)returns allM-unifiers between termmand theLFunof subterms ofh. The pseu- docode formatchis given in Algorithm 3. An auxiliary functionunifyis used in the pseudocode. GivenλCcontextΓ, variable setMand twoλCterms t1, t2,...

  52. [60]

    maxHeartbeats

    Given contextΓand termsm, h,matchInst(Γ;m, h)computes all instances of the hypothesishwhich has some subterm whoseLFunisβη-equivalent tom. To do this,matchInstintroduces all leading non-prop∀quantifiers into the context (as free variables), collects all the newly introduced fr...

  53. [61]

    Import the entire Mathlib4

  54. [62]

    simp” attribute. Suppose a theoremTin Mathlib4 is tagged with “simp

    For each theoremTinTs, collect all the theoremsh 1, . . . , hn used in the proof ofT. Then, call the underlying tactic function oftacon the statement ofTand record the result. Iftacaccepts premises, supplyh 1, . . . , hn as the list of premises to the under- lying tactic funct...

  55. [63]

    Retrieve the content ofF

  56. [64]

    maxHeartbeats

    For each commandCinF: (a) Record the environmentEbefore executingC.Econtains all the constants declared by commands prior toC. (b) Run commandCand record the constantsc1, . . . , cn declared by it. (c) Record the environmentE′. (d) Set the environment toE. This effectively rem...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.