Lean-SMT: An SMT tactic for discharging proof goals in Lean
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916749887143936 |
|---|---|
| author | Mohamed, Abdalrhman Mascarenhas, Tomaz Khan, Harun Barbosa, Haniel Reynolds, Andrew Qian, Yicheng Tinelli, Cesare Barrett, Clark |
| author_facet | Mohamed, Abdalrhman Mascarenhas, Tomaz Khan, Harun Barbosa, Haniel Reynolds, Andrew Qian, Yicheng Tinelli, Cesare Barrett, Clark |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_15796 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Lean-SMT: An SMT tactic for discharging proof goals in Lean Mohamed, Abdalrhman Mascarenhas, Tomaz Khan, Harun Barbosa, Haniel Reynolds, Andrew Qian, Yicheng Tinelli, Cesare Barrett, Clark Logic in Computer Science 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. |
| title | Lean-SMT: An SMT tactic for discharging proof goals in Lean |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.15796 |