SMT Integration

Stream: general

[Wojciech Nawrocki]

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]

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]

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

[Simon Cruanes]

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

[Simon Hudon]

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

[Simon Cruanes]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Cruanes]

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]

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]

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

[Simon Hudon]

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