Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

Lean-SMT: An SMT tactic for discharging proof goals in Lean

T0 review · 3 major / 4 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-SMT is a tactic that lets Lean use the SMT solver cvc5 to prove goals, then reconstructs cvc5's proof as a native Lean proof accepted by Lean's kernel.

desk verdict A genuinely new, kernel-checked SMT proof-replay tactic for Lean with a solid soundness core; the biggest gap is that the evaluation never measures the Lean goals the tool is actually meant to discharge. read the letter →

arxiv 2505.15796 v1 pith:ZIPDR35A submitted 2025-05-21 cs.LO

Abdalrhman Mohamed , Tomaz Mascarenhas , Harun Khan , Haniel Barbosa , Andrew Reynolds , Yicheng Qian , Cesare Tinelli , Clark Barrett This is my paper · ORCID
classification cs.LO
keywords LeanSMTsolvingproofreconstructioncvc5CPCformatSledgehammerassistantsformalverification
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-SMT is a tactic that lets the Lean proof assistant hand proof goals to the SMT solver cvc5, then turns cvc5's proof into a proof Lean's own kernel accepts. If it works as described, Lean gains Sledgehammer-style automation for goals in first-order fragments such as uninterpreted functions, linear integer and real arithmetic, and quantifiers. The paper's central claim is that this can be done soundly by replaying each step of cvc5's proof inside Lean, so the trusted base stays small, and fast enough to be useful: it keeps pace with Sledgehammer's SMT backend on standard benchmarks and with verified checkers on SMT-LIB problems. The authors present this as a first step toward a full Lean hammer.

What carries the argument

The central mechanism is proof replay of cvc5's CPC proofs: each inference rule is reconstructed in Lean either by a pre-proved theorem (163 rules), a specialized tactic (37 rules), or a verified reflective program (5 rules), and every reconstructed step is checked by the kernel. CPC is cvc5's proof calculus, whose rules have premises, arguments, and decidable side conditions. The pipeline also includes proof-producing preprocessing via lean-auto and a translation step that maps Lean types and constructs to SMT-LIB sorts and theories.

What would settle it

Run lean-smt on a large sample of goals drawn from Mathlib rather than Sledgehammer-translated Isabelle problems, and count how many fail solely because cvc5's proof uses a CPC rule outside the supported ~200; if a substantial fraction fail, the claim that the supported rules cover the most common Lean goals is false.

Watch

Extended reading notes

Core claim

The paper's central claim is that a Lean tactic can bridge dependent type theory and SMT by preprocessing a goal into first-order form, translating it to SMT-LIB, asking cvc5 for a proof in the Cooperating Proof Calculus (CPC), and replaying that proof step by step as native Lean proof steps, so that Lean's kernel, not cvc5, is the ultimate soundness guarantee. The authors further claim that this design gives Lean a Sledgehammer-style SMT integration with a smaller trusted core than verified checkers like SMTCoq, at competitive performance.

Load-bearing premise

The load-bearing premise is that the roughly 200 supported cvc5 proof rules cover the goals that arise in ordinary Lean work, a claim not tested on Lean-native benchmarks.

Editorial extensions

If this is right

  • Goals in the supported fragments (uninterpreted functions, linear integer and real arithmetic, mixed linear arithmetic) can be discharged automatically with kernel-checked proofs.
  • Soundness of the overall tactic depends on Lean's kernel, not on trusting cvc5's implementation.
  • Compared with veriT+Sledgehammer and Duper on Sledgehammer benchmarks, lean-smt proves more goals in the tested set.
  • As a standalone checker, lean-smt verifies about 71% of cvc5 proofs in supported SMT-LIB fragments, within an order of magnitude of Ethos in time.
  • The proof-replay architecture is easier to adapt to cvc5's evolving proof rules than a fully verified checker like SMTCoq.

Reading between the lines

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

  • A Lean-native benchmark suite would be needed before the coverage claim is settled; the paper itself notes that no dedicated Lean benchmark set is used.
  • The same replay architecture could, in principle, be fitted to other proof-producing SMT solvers that emit a step-by-step calculus, since only the rule-to-Lean mapping would change.
  • If lean-smt matures with premise selection and broader theory support, it could form the engine of a full Lean hammer comparable to Sledgehammer.
  • The empty-type soundness check is a hidden precondition: any goal whose translation names a sort with no nonempty Lean instance will fail, so the tactic's coverage is tied to how often that check succeeds.
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 / 4 minor

Summary. The paper presents Lean-SMT, a tactic for the Lean proof assistant that translates a proof goal into an SMT-LIB problem, invokes the cvc5 solver, and reconstructs the resulting CPC proof as a native Lean proof that is checked by Lean's kernel. The pipeline consists of proof-producing preprocessing using lean-auto and custom normalization, translation to SMT-LIB with a mechanism to address the different non-emptiness assumptions of SMT-LIB sorts and Lean types, step-by-step reconstruction using 163 theorems, 37 specialized tactics, and 5 reflective procedures, and final kernel verification. The evaluation covers 5,000 Sledgehammer benchmarks derived from Isabelle/HOL and 24,817 SMT-LIB benchmarks from the supported fragments, comparing Lean-SMT against veriT+Sledgehammer, Duper, Ethos, and SMTCoq. The paper reports competitive performance and claims a smaller trusted core for Lean-SMT.

Significance. If the central claims hold, this is a significant systems contribution: it provides Lean with a Sledgehammer-style SMT integration whose successful replays are verified by Lean's kernel. The reconstruction theorems and the reflective normalizer are machine-checked, and the paper is careful to report both 'Checked' and 'Checked (no holes)' numbers. The evaluation against established baselines on standard benchmarks gives meaningful evidence about the viability of the proof-replay architecture. The main weakness is empirical: the paper asserts that the supported subset of proof rules covers the most common goals in Lean, but the evaluation does not use Lean-specific benchmarks, leaving the central usefulness claim for Lean developments unmeasured.

major comments (3)
  1. [Section 3.3] The claim that the supported subset of about 200 CPC proof rules (~30% of the format) 'suffices to support the most common proof goals in Lean' is not substantiated by the evaluation. Section 4 uses only Sledgehammer benchmarks derived from Isabelle/HOL and SMT-LIB problems in the supported fragments; Section 5 lists 'creating a dedicated Lean benchmark set' as future work. Since the tactic's stated purpose is discharging proof goals arising in Lean, the paper should either provide evidence on a corpus of Lean goals (for example, representative goals from Mathlib or a dedicated Lean benchmark suite) or explicitly qualify the claim to the supported fragment. This is an empirical gap, not a soundness flaw.
  2. [Section 4.2, Table 2] The prose states that 'lean-smt successfully verified 15,271 proofs (71%)', but this number is the 'Checked' column, which includes proofs with holes. The complete-proof count is 'Checked (no holes)' = 14,099. Because the standalone proof-checking claim concerns verifying complete CPC proofs, the headline success rate should be the no-holes figure, with the looser count clearly labeled as partial checking. As written, the main text overstates the checker's coverage.
  3. [Section 3.2] The handling of the empty-type discrepancy is described only at a high level: 'The reconstruction stage ensures soundness by failing if a proof step depends on a type being non-empty and Lean cannot establish that the type is an instance of the type class of non-empty types.' The paper should specify which CPC rules or proof steps are treated as non-emptiness-sensitive, how the corresponding Lean condition is checked, and why the check covers indirect uses of sort non-emptiness such as quantifier instantiation. Because the Lean kernel checks the final proof, this is a rigor gap in the description rather than a demonstrated unsoundness, but it is load-bearing for the translation's correctness argument.
minor comments (4)
  1. [Section 5] The conclusion mentions Carcara as a state-of-the-art proof checker, but no reference for Carcara is given in the bibliography.
  2. [Section 4.1] The paper reports that Lean-SMT takes under a second to replay proofs for 98% of the Sledgehammer benchmarks, but the figures do not separate solver time from reconstruction time. A breakdown would help quantify the reconstruction overhead more precisely.
  3. [Appendix B, Table 1] The table caption says 'baseline Seventeen Provers benchmarks', while Section 4.1 describes the set as 5000 SMT problems generated by Sledgehammer. Making the provenance explicit in the caption would avoid confusion.
  4. [Example 6] The displayed theorem statement for denote_eq_from_toPoly_eq has a formatting issue: 'e1.denote ictx rctx' appears to run together and is missing a space or a variable separator.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the reconstruction chain is kernel-checked and evaluated against external benchmarks.

full rationale

The paper's central claim is that Lean-SMT can translate Lean goals to SMT-LIB, obtain cvc5 proofs, and reconstruct native Lean proofs accepted by the kernel. This derivation chain is self-contained: the preprocessing steps are proof-producing in Lean, the translation to SMT-LIB is described with explicit examples, and every reconstructed proof is checked by Lean's kernel. No parameter is fitted to a subset of data and then renamed as a prediction; the evaluation compares against established external baselines (Sledgehammer's veriT backend, Ethos, SMTCoq) on Sledgehammer and SMT-LIB benchmarks. The self-citations to cvc5, Ethos, and SMTCoq are normal system references and are not load-bearing for the central soundness or performance claims. The paper's Section 3.3 statement that the roughly 200 supported CPC rules 'suffice to support the most common proof goals in Lean' is an empirical assumption, and Section 5 concedes that a dedicated Lean benchmark set is future work, but this is a coverage limitation rather than a circular step. Overall, no claim reduces by construction to its own inputs, so the circularity score is 0.

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

The system's soundness rests on Lean's kernel and on the correctness of the mapping from CPC proof rules to Lean justifications. The main non-validated assumption is that the supported rule subset covers common Lean goals. No free parameters or invented entities are involved.

assumptions (4)
  • domain assumption Lean's kernel is sound and consistently implements dependent type theory with the standard classical axioms (propext, funext, choice, quotient).
    The entire reconstruction approach relies on the kernel accepting a proof term implying the goal is provable; if the kernel were unsound, the 'proof' would not establish truth. Invoked throughout Sections 3.3 and 4.
  • domain assumption The semantics of each supported CPC proof rule is correctly captured by the corresponding Lean theorem or tactic.
    Reconstruction maps each cvc5 proof step to a Lean justification; a mismatch would produce a kernel-rejected or wrong proof. Discussed in Section 3.3, e.g., RESOLUTION and ARITH_MULT_TANGENT.
  • domain assumption The translation from the preprocessed Lean FOL fragment to SMT-LIB preserves satisfiability, with the non-empty sort issue resolved by the Nonempty check.
    Section 3.2 states SMT-LIB sorts are non-empty while Lean allows empty types, and soundness is restored by failing when non-emptiness cannot be proved.
  • domain assumption The 200 supported proof rules cover the most common proof goals in Lean.
    Section 3.3: 'We prioritized this subset because it suffices to support the most common proof goals in Lean' but this is not validated with Lean-specific benchmarks.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Lean-SMT: An SMT tactic for discharging proof goals in Lean." pith.science (2026). https://pith.science/paper/ZIPDR35A

@misc{pith2026250515796,
  author       = {Pith},
  title        = {Pith review of: Lean-SMT: An SMT tactic for discharging proof goals in Lean},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZIPDR35A}},
  note         = {Machine review of arXiv:2505.15796}
}
read the original abstract

Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic in Isabelle/HOL. A key aspect of Sledgehammer is the use of proof-producing SMT solvers to prove a translated proof goal and the reconstruction of the resulting proof into valid justifications for the original goal. We present Lean-SMT, a tactic providing this functionality in Lean. We detail how the tactic converts Lean goals into SMT problems and, more importantly, how it reconstructs SMT proofs into native Lean proofs. We evaluate the tactic on established benchmarks used to evaluate Sledgehammer's SMT integration, with promising results. We also evaluate Lean-SMT as a standalone proof checker for proofs of SMT-LIB problems. We show that Lean-SMT offers a smaller trusted core without sacrificing too much performance.

Figures

Figures reproduced from arXiv: 2505.15796 by the authors.

Figure 1
Figure 1. Architecture of the lean-smt tactic. proof is then reconstructed as a proof in Lean for the input formula. The light￾green boxes represent the proofs used during the reconstruction stage, which correspond directly to the formulas (light-blue) processed during the translation stage. The dashed lines emphasize this correspondence. The preprocessor module converts the initial input F into an intermediate form F ′ , sim… view at source ↗
Figure 2
Figure 2. (a) shows the performance of lean-smt on Sledgehammer benchmarks, while (b) compares proof checking performance of lean-smt with Ethos. 4.1 Isabelle Sledgehammer Benchmarks We evaluate lean-smt on SMT problems generated by Isabelle’s Sledgeham￾mer. We chose these benchmarks over other options (e.g., Lean’s MathLib) due to Lean’s lack of a premise selection mechanism, which is crucial for reducing false positives (i.… view at source ↗
Figure 3
Figure 3. Figure (a) shows the performance of lean-smt on supported SMT-LIB fragments, while Figure (b) shows the performance on the quantifier-free subset. Note that both lean-smt and SMTCoq are highly trustworthy, since they both rely on small kernels. However, SMTCoq’s code extraction mechanism, which extracts OCaml code from verified Coq code, has to be trusted as well. The trusted base for Ethos, besides its kernel, also… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Implementation of the sumBounds tactic 1 def combineBounds (pf1 pf2 : Expr) : MetaM Expr := do 2 let t1 ← inferType pf1 3 let t2 ← inferType pf2 4 let rel1 ← getRel t1 5 let rel2 ← getRel t2 6 let opType1 ← getOperandType t1 7 let opType2 ← getOperandType t2 8 let (pf1…

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

34 extracted references · 22 canonical work pages · cited by 1 Pith paper

  1. [1]

    Avigad, J., de Moura, L., Kong, S., Ullrich, S.: Theorem proving in lean 4, uRL: https://leanprover.github.io/theorem_proving_in_lean4/

    work page

  2. [2]

    Phd-thesis - re- search and graduation internal, Vrije Universiteit Amsterdam (Jan 2024)

    Baanen, A.: Formalizing Fundamental Algebraic Number Theory. Phd-thesis - re- search and graduation internal, Vrije Universiteit Amsterdam (Jan 2024). https: //doi.org/10.5463/thesis.541

    work page doi:10.5463/thesis.541 2024

  3. [3]

    In: Fisman, D., Rosu, G

    Barbosa, H., Barrett, C.W., 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 Construction and Analysis of Systems (TACA...

    2022

  4. [4]

    In: Blanchette, J., Kovács, L., Pattinson, D

    Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Barrett, C.W.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) International Joint Confer- ence on Automated Reasoning (IJCAR). Lec...

    work page doi:10.1007/978-3-031-10769-6_3 2022

  5. [5]

    In: Gopalakrishnan, G., Qadeer, S

    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Com- puter Aided Verification (CAV). pp. 171–177. Springer (2011). https://doi.org/10. 1007/978-3-642-22110-1_14, http://dx.doi.org/10.1007/978-3-642-22110-1_14 Lean-SMT: An SMT tactic for discharging pro...

    doi:10.1007/978-3-642-22110-1_14 2011

  6. [6]

    Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017), available at www.SMT-LIB.org

    work page 2017

  7. [7]

    Texts in Theoretical Computer Science

    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Develop- ment - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004). https://doi.org/10.1007/ 978-3-662-07964-5

    work page 2004

  8. [8]

    In: Bjørner, N.S., Sofronie-Stokkermans, V

    Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: Bjørner, N.S., Sofronie-Stokkermans, V. (eds.) Automated Deduc- tion - CADE-23 - 23rd International Conference on Automated Deduction, Wro- claw, Poland, July 31 - August 5, 2011. Proceedings. Lecture Notes in Com- puter Science, vol. 6803, pp. 116–130. Springer (2011...

    work page doi:10.1007/978-3-642-22438-6_11 2011

Show all 34 references
  1. [9]

    Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning9(1), 101–148 (2016)

    2016

  2. [10]

    Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers.In:Boogie2011:FirstInternationalWorkshoponIntermediateVerification Languages. pp. 53–64 (2011)

    2011

  3. [11]

    In: Schmidt, R.A

    Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: An Open, Trustable and Efficient SMT-Solver. In: Schmidt, R.A. (ed.) Conference on Auto- mated Deduction (CADE). Lecture Notes in Computer Science, vol. 5663, pp. 151–156. Springer (2009). https://doi.org/10.10...

    2009 doi

  4. [12]

    grand unification

    Castelvecchi, D.: Mathematicians welcome computer-assisted proof in “grand unification” theory. Nature 595 (06 2021). https://doi.org/10.1038/ d41586-021-01627-2

    2021

  5. [13]

    In: Bertot, Y., Kut- sia, T., Norrish, M

    Clune, J., Qian, Y., Bentkamp, A., Avigad, J.: Duper: A Proof-Producing Su- perposition Theorem Prover for Dependent Type Theory. In: Bertot, Y., Kut- sia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Pro...

    2024 doi

  6. [14]

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

    mathlib Community, T.: 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

  7. [15]

    In: Andronick, J., de Moura, L

    Desharnais, M., Vukmirovic, P., Blanchette, J., Wenzel, M.: Seventeen provers under the hammer. In: Andronick, J., de Moura, L. (eds.) 13th International Con- ference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Is- rael. LIPIcs, vol. 237, pp. 8:1–8:18. ...

    2022 doi

  8. [16]

    In: Majumdar, R., Kunčak, V

    Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.: Smtcoq: A plug-in for integrating smt solvers into coq. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 126–133. Springer International Pub- lishing, Cham (2017)

    2017

  9. [17]

    Academic Press, 2 edn

    Enderton, H.B.: A mathematical introduction to logic. Academic Press, 2 edn. (2001) 14 Mohamed et al

    2001

  10. [18]

    In: Ka- pur, D

    Gonthier, G.: The four colour theorem: Engineering of a formal proof. In: Ka- pur, D. (ed.) Computer Mathematics, 8th Asian Symposium, ASCM 2007, Sin- gapore, December 15-17, 2007. Revised and Invited Papers. Lecture Notes in Computer Science, vol. 5081, p. 333. Springer (2007...

    2007 doi

  11. [19]

    Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A for...

    2015

  12. [20]

    Hurd, J.: First-order proof tactics in higher-order logic theorem provers in proc (2003), https://api.semanticscholar.org/CorpusID:11201048

    2003

  13. [21]

    In: Naumowicz, A., Thiemann,R.(eds.)InteractiveTheoremProving(ITP).LIPIcs,vol.268,pp.19:1– 19:22

    Jakubuv, J., Chvalovský, K., Goertzel, Z.A., Kaliszyk, C., Olsák, M., Piotrowski, B., Schulz, S., Suda, M., Urban, J.: Mizar 60 for mizar 50. In: Naumowicz, A., Thiemann,R.(eds.)InteractiveTheoremProving(ITP).LIPIcs,vol.268,pp.19:1– 19:22. Schloss Dagstuhl - Leibniz-Zentrum fü...

    2023 doi

  14. [22]

    Kaliszyk, C., Urban, J.: Hol(y)hammer: Online ATP service for HOL light. Math. Comput. Sci. 9(1), 5–22 (2015). https://doi.org/10.1007/S11786-014-0182-0, https://doi.org/10.1007/s11786-014-0182-0

    2015 doi

  15. [23]

    Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elka- duwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Win- wood, S.: sel4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010). https://doi....

    2010

  16. [24]

    In: Finkbeiner, B., Kovács, L

    Lachnitt, H., Fleury, M., Aniva, L., Reynolds, A., Barbosa, H., Nötzli, A., Barrett, C.W., Tinelli, C.: Isarare: Automatic verification of SMT rewrites in isabelle/hol. In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for Construction and Analysis of Systems (TACAS),...

    2024 doi

  17. [25]

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

    Limperg, J., From, A.H.: Aesop: White-box best-first proof search for lean. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 253–266. CPP 2023, Association for Computing Ma- chinery, New York, NY, USA (2023). https://doi.org...

    2023

  18. [26]

    Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First proto- type. Inf. Comput.204(10), 1575–1596 (2006). https://doi.org/10.1016/J.IC.2005. 05.010, https://doi.org/10.1016/j.ic.2005.05.010

    2006 doi

  19. [27]

    In: Platzer, A., Sutcliffe, G

    de Moura, L., Ullrich, S.: The lean 4 theorem prover and programming lan- guage. In: Platzer, A., Sutcliffe, G. (eds.) Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 12699, pp. 625–635. Springer (2021). https://doi.org/10.1007/978-3-030-79876...

    2021 doi

  20. [28]

    In: 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4-6, 2020

    Nelson, L., Geffen, J.V., Torlak, E., Wang, X.: Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the linux kernel. In: 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November ...

    2020

  21. [29]

    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002) Lean-SMT: An SMT tactic for discharging proof goals in Lean 15

    2002

  22. [30]

    In: Griggio, A., Rungta, N

    Nötzli, A., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C.W., Tinelli, C.: Reconstructing fine-grained proofs of rewrites using a domain-specific language. In: Griggio, A., Rungta, N. (eds.) Formal Methods In Computer-Aided Design (FMCAD). pp. 65–74. IEEE (20...

    2022 doi

  23. [31]

    Piotrowski, B., Mir, R.F., Ayers, E.: Machine-learned premise selection for lean (2023), https://arxiv.org/abs/2304.00994

    2023 arXiv

  24. [32]

    CoRRabs/2107.02354 (2021), https://arxiv

    Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: Towards a generic SMT proof format (extended abstract). CoRRabs/2107.02354 (2021), https://arxiv. org/abs/2107.02354

    2021 arXiv

  25. [33]

    In: Platzer, A., Sutcliffe, G

    Schurr, H., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduc- tion - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedin...

    2021 doi

  26. [34]

    [sumBounds]: invalid relation

    Tao, T.: Machine assisted proof. AMS Notices72(1), 86–95 (2025). https://doi. org/10.1090/noti3041, https://doi.org/10.1090/noti3041 16 Mohamed et al. Fig.4: Implementation of thesumBounds tactic 1 def combineBounds (pf 1 pf2 : Expr) : MetaM Expr := do 2 let t 1 ← inferType pf...

    2025 doi

Pith tools

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