LeanHammer?

Stream: general

[Albert Jiang]

Do people know if there is a hammer for lean under construction?
Thanks!

[Henrik Böving]

Hammers for dependently typed languages seem to be a rather complicated problem, the Coq people got something going here https://coqhammer.github.io/, the closest we have right now that I know of is library_search, not aware of anyone doing a lean hammer.

[Gabriel Ebner]

I did some work on a leanhammer for Lean 3 some time ago, but in the end it didn't work out due to performance issues. You can watch my talk/slides from FoMM20: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/abstracts.html I'm expecting it to work much butter in Lean 4, but so far I haven't found any time to pick up the work again.

[Albert Jiang]

Thank you both!

[Albert Jiang]

Henrik Böving said:

Hammers for dependently typed languages seem to be a rather complicated problem, the Coq people got something going here https://coqhammer.github.io/, the closest we have right now that I know of is library_search, not aware of anyone doing a lean hammer.

It does look like https://leanprover-community.github.io/mathlib_docs/tactic/suggest.html#top library_search and suggest are very close to what I was looking for. Thanks!