Implements QuerySMT, a Lean tactic leveraging cvc5 SMT hints to improve Lean's internal automation.
Abstract
There are several paradigms for integrating interactive and automated theorem provers, combining the convenience of powerful automation with strong soundness guarantees. We introduce a new approach for reconstructing proofs found by SMT solvers which we intend to be complementary with existing techniques. Rather than verifying or replaying a full proof produced by the SMT solver, or at the other extreme, rediscovering the solver's proof from just the set of premises it uses, we explore an approach which helps guide an interactive theorem prover's internal automation by leveraging derived facts during solving, which we call hints. This makes it possible to extract more information from the SMT solver's proof without the cost of retaining a dependency on the SMT solver itself. We implement a tactic in the Lean proof assistant, called QuerySMT, which leverages hints from the cvc5 SMT solver to improve existing Lean automation. We evaluate QuerySMT's performance on relevant Lean benchmarks, compare it to other tools available in Lean relating to SMT solving, and show that the hints generated by cvc5 produce a clear improvement in existing automation's performance.
Problem
Integrating SMT solvers with interactive theorem provers requires either verifying full SMT proofs (expensive) or rediscovering proofs from premises alone (unreliable). A middle ground that leverages derived intermediate facts from the solver to guide the prover is unexplored.
Approach
The authors develop querysmt, a Lean tactic that sends goals to the cvc5 SMT solver and receives back hints (preprocessing lemmas, theory lemmas, rewrite steps) rather than full proofs. These hints guide Lean's internal automation (omega, simp, norm_num) to reconstruct the proof. The pipeline includes preprocessing, translation to SMT-LIB via lean-auto, and hint interpretation back into Lean expressions.
Figure 1: Overview of the querysmt tactic. Blue boxes indicate Lean stages. Yellow boxes indicate SMT stages. Stages in the green area directly transform the Lean goal and must be replayed in the final suggested proof script. Stages in the purple area do not transform the goal and therefore do not need to be replayed. Red dotted lines indicate information transfer between stages.
Results
The tactic produces self-contained Lean proof scripts that do not depend on external solvers at verification time. The approach is complementary to existing reconstruction techniques, offering a practical balance between full proof checking and premise-only methods.
