Comparison with Sledgehammer

Stream: general

[Martin Dvořák]

How would you compare automated claim-proving features in Lean with Sledgehammer in Isabelle? Do they aim for something completely different? And are they comparable for practical purposes?

[Johan Commelin]

Currently sledgehammer is better than that auto-provers in lean. There are serious plans for a lean-hammer in lean 4 though.

[Chris B]

Gabriel Ebner did work on this in Lean 3 a while back. I believe his conclusion was that further work would have to wait for Lean 4 for performance reasons. The slides are in the description:

https://www.youtube.com/watch?v=WydyJJYKyTs

[Martin Dvořák]

Is the following statement right? I want to mention this comparison in my research proposal.

Sledgehammer combines what Lean can do using simp and library\_search into one powerful tool. In this regard, Lean lacks behind Isabelle.

[Alex J. Best]

This sounds a bit too simplistic, I think the last sentence is correct, but Sledgehammer does more than just simp and library search together by far which is what your first sentence seems to imply without any context

[Arthur Paulino]

Also, as Kevin said, Lean allows the implementation of tactics in Lean itself. So it doesn't seem to be the case that Lean lacks behind. It's just that we haven't implemented such a tactic yet. Does it make sense?

[Arthur Paulino]

Lean's kernel is very small. Thus, depending on what you call "Lean", it may lack a lot of things!

[Alex J. Best]

By that logic Lean can do anything though, implementing a decent sledgehammer is a huge amount of work, and the Isabelle people have been working on it for over 10 years. The sledgehammer isn't in the kernel of isabelle either so I don't think saying we lack behind is unfair, they really do have a tool we all wish we had

[Martin Dvořák]

To make it correct, I better say that the Lean's tooling lacks behind Isabelle's tooling, ok?

[Arthur Paulino]

In this sense, regarding sledgehammer, yes. I might be wrong in my way of thinking, but I do believe that Lean's tooling also has some cards that Isabelle doesn't? It's a bit hard to weigh everything fairly.

[Arthur Paulino]

Maybe just for the sake of safety and compromise with generalizations, be more specific and direct about this particular tool (or other tools) that we don't have yet.