33
$\begingroup$

When proving things in a theorem prover, I am often using sizable libraries that I don’t know by heart, so it is crucial to be effective in discovering existing theorems.

What are the best approaches here? Both within the IDE (likely less friction, but also likely restricted to theorems from the currently imported modules), but also on the web (to find more stuff)? Is there something like Hoogle that allows me to search for concrete types, or something like Isabelle’s find_theorem, where I can search for theorems by name, by a pattern expression LHS of simplification rule, and other clever ways?

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ So, we need an answer that at least covers the library_search and suggest tactics and at the same time explains their use cases as well as how to use them (suggest in particular is difficult to use until you have some experience decoding names in Lean). $\endgroup$
    – march
    Commented Feb 11, 2022 at 19:08
  • 2
    $\begingroup$ It sometimes works well to enter keywords in the search box at github.com/leanprover-community/mathlib or the one at leanprover-community.github.io/mathlib_docs. $\endgroup$
    – Neil Strickland
    Commented Feb 15, 2022 at 13:23
  • $\begingroup$ There is also now moogle.ai which is an AI powered search engine for Lean theorems. $\endgroup$
    – Jason Rute
    Commented Nov 19, 2023 at 22:44

3 Answers 3

Reset to default
16
$\begingroup$

I use three strategies to find existing lemmas: the exact? tactic, the gptf tactic and guessing the name based on mathlib naming conventions.

exact?

exact? is a mathlib tactic, not a Lean tactic. (It was earlier called library_search.) It tries to find a single lemma from the library to solve the current goal, also using local hypotheses to fill in arguments. To make the best use of this tactic, make sure that:

  • The current context doesn't have many extraneous assumptions. You might want to use the clear and the clear_except tactic to remove unnecessary assumptions. If you don't do this, exact? might timeout.
  • You have introduced all necessary variables and hypotheses. If your goal has forall and imply then it's very likely that library_search won't be able to find anything.
  • The assumptions are in simp normal form.
  • exact? will only succeed if it can close the goal. If you would also like candidate incomplete solutions (i.e. where a library lemma can be applied to the goal, but then that lemma has hypotheses that can not be filled from the local context) then use apply? instead.
  • There is now a relative of apply? for rewriting, called rw?, which will try to rewrite the current goal by a single lemma from the library, returning multiple candidates if none close the goal.

gptf

Unfortunately, this tactic is no longer a thing.

This tactic uses artificial intelligence. It is faster than library_search, and sometimes smarter. When you are stuck, sometimes gptf can give helpful hints. In addition to finding mathlib lemmas, sometimes gptf can suggest tactics and complete proofs. Follow the instructions on GitHub to get access to this tactic.

mathlib naming conventions

Please familiarize yourself with the naming conventions. You can often find lemmas by guessing its name and letting autocomplete help you.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ I've not been able to use gptf for a while in the latest versions - do you know how to make it work? $\endgroup$
    – It'sNotALie.
    Commented Feb 12, 2022 at 13:26
  • 1
    $\begingroup$ Also, it may be worth mentioning suggest and the using ... variants of both of these $\endgroup$
    – It'sNotALie.
    Commented Feb 12, 2022 at 13:27
  • 1
    $\begingroup$ How does library_search relate to suggest? I often find that the latter finds a small exact … proof, while the former doesn’t produce anything. $\endgroup$
    – Joachim Breitner
    Commented Feb 12, 2022 at 13:31
  • $\begingroup$ I generally find that library_search works better if I restate the desired lemma on its own and use the tactic there, rather than using it in the midst of a complex proof. $\endgroup$
    – Neil Strickland
    Commented Feb 15, 2022 at 13:26
  • $\begingroup$ Which one of this is the closest to the Search command in Coq? $\endgroup$
    – Agnishom Chattopadhyay
    Commented Aug 28, 2023 at 21:37
8
$\begingroup$

Bothered by the lack of something like find_theroems and Hoogle, I have implemented a search engine that has some of its features; Loogle.

Loogle web interface

It can search by occurring constants, name substrings or aribtrary patterns, and can be accessed using the web page, a VS Code extension, is integrated into lean.nvim or can be used locally via a CLI, a Lean command or (again) a browser interface.

Improve this answer
$\endgroup$
4
$\begingroup$

There's moogle.ai. It does semantic search over mathlib

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.