mathlib

mathlib copied to clipboard

The recommend tactic searches for lemmas in the current environment that look like they could be useful to prove the current goal.

It is based on premise selection heuristic used in CoqHammer, with a preprocessing step that removes type arguments, type class instances, etc. This heuristic analyzes the proofs of the theorems in the environment: it will suggest lemmas that have been used in proofs of similar theorems as the current goal.

The heuristic is completely syntactic; it won't unfold definitions during the search, and doesn't know about types and type classes.

As requested on Zulip: https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20lean.3Amaster/near/274918133

---

The code is based on my leanhammer prototype from 2019.

I tried it out on some random parts of mathlib. The results are very uneven. Sometimes it finds just the right lemma (I've added one example in the second commit). In other parts of the library it gets completely confused, for lack of a better word, and doesn't return anything useful or related.

I don't plan on developing the Lean 3 version any further. (The interesting code is in C++ which makes the turnaround pretty slow since we have to do a Lean release for every change.)

I'm editorialising a little here by marking this as not-too-late, just as a reminder/hope that we'll get around to having this in Lean 4! :-)

@semorrison, can we consider this replaced by have??

@semorrison, can we consider this replaced by have??

I don't think so.