Zulip Chat Archive

Stream: general

Topic: LeanHammer?


Albert Jiang (May 11 2022 at 17:41):

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

Henrik Böving (May 11 2022 at 17:46):

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 (May 11 2022 at 17:56):

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 (May 11 2022 at 19:04):

Thank you both!

Albert Jiang (May 11 2022 at 19:07):

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!


Last updated: Dec 20 2023 at 11:08 UTC