## Stream: general

### Topic: SMT Integration

#### Wojciech Nawrocki (Jan 25 2019 at 19:47):

What's the status of integrating SMT solvers with Lean? There are some references to it in the documentation, (e.g. https://leanprover.github.io/reference/tactics.html#the-smt-state) but all are empty. It would be nice to have some automatic solving.

#### Simon Hudon (Jan 25 2019 at 19:51):

The smt tactics are not very much used. I just started this week looking at wrapping veriT into Lean tactics and as far as I know, that's the only such work going on in Lean

#### Simon Hudon (Jan 25 2019 at 19:53):

Maybe Jasmin Blanchette's team has something related in the works but I don't know any details.

#### Simon Cruanes (Jan 25 2019 at 20:06):

What fragment do you plan to encode into SMTLIB, and how?

#### Simon Hudon (Jan 25 2019 at 20:07):

Right now, I haven't settled on a fragment, I'm just looking at building the interface for now.

#### Simon Cruanes (Jan 25 2019 at 20:20):

I suppose the closest existing thing is SMTCoq, especially regarding proof reconstruction, but that's a lot of work

#### Simon Hudon (Jan 25 2019 at 21:35):

I'm looking at SMTCoq and Blanchette's work for Isabelle. I think it's probably work worth doing.

#### Simon Hudon (Jan 25 2019 at 21:36):

I'm building proof obligation generators in Lean and smt solvers are useful to discharge those

#### Simon Cruanes (Jan 25 2019 at 21:36):

I know Jasmin has been talking about an independent Sledgehammer-like tool that could be shared between proof assistants, but that'd be even more work…
If you do it directly in Lean it'll be easier to reconstruct proofs.

#### Simon Hudon (Jan 25 2019 at 21:44):

That's my opinion too. I think whereas Jasmin's project is more general and long term, mine is to address an immediate need and I'm ok with doing it imperfectly at first

#### Gabriel Ebner (Jan 25 2019 at 21:49):

There is https://github.com/leanprover/smt2_interface from quite some time ago, but it doesn't generate proofs.

#### Simon Hudon (Jan 25 2019 at 21:57):

Thanks for the link! I was trying to find it again but didn't look in the most obvious place

Last updated: May 17 2021 at 22:15 UTC