Is there a hammer in Lean?

Stream: lean4

[Shaonan Wu]

Dear all,
I am curious if there is a powerful tool in the Lean theorem prover similar to Isabelle's sledgehammer in Lean theorem prover.

[Ruben Van de Velde]

I'm sure there's numerous discussion of such things that can be found in the archives of this zulip instance. Without knowing what sledgehammer does, you might be interested in aesop

[Shaonan Wu]

Ruben Van de Velde said:

I'm sure there's numerous discussion of such things that can be found in the archives of this zulip instance. Without knowing what sledgehammer does, you might be interested in aesop

Thank you. It helps a lot

[Notification Bot]

Shaonan Wu has marked this topic as resolved.

[Joachim Breitner]

Unless I am mistaken, aesop is more like Isabelle's auto, and lean-auto is more like Isabelle's sledgehammer

[Notification Bot]

Shaonan Wu has marked this topic as unresolved.