Relationship between Lean and SMT solvers

Stream: lean4

[Bach Hoang]

Hi,

I want to know how Lean4 can be used as an SMT solver or connected to an SMT solver (e.g. Z3).

Thanks for your help.

[Kim Morrison]

This is "research project level", and the best place to start may be searching the zulip for "smt", and writing here a summary of what you found. :-) Or, possibly, the people working on such projects may pop up here and summarise current progress.

[Kim Morrison]

Lean does now ship with bv_decide (a decision procedure for fixed width bitvector problems), that is backed by a SAT solver (cadical), but this is a very different question that SMT solvers, where reconstructing a proof in Lean is a very different matter.