add post on searching for lemmas #75
Open
+101
−0
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
This is perhaps a bit out of date, but if anyone wants to pick this back up or make changes, feel free! |
BoltonBailey
commented
Nov 7, 2024
BoltonBailey
commented
Nov 7, 2024
BoltonBailey
commented
Nov 7, 2024
BoltonBailey
commented
Nov 12, 2024
BoltonBailey
commented
Nov 12, 2024
| --- | ||
| author: 'Bolton Bailey' | ||
| category: 'Overview' | ||
| date: 2024-06-01 13:35:44 UTC-08:00 |
|
|
||
|  | ||
|
|
||
| [Moogle](https://www.moogle.ai/) is a semantic search engine for Mathlib developed by [Morph labs](https://morph.so/). One enters searches in natural language and the engine tries to turn up theorems that match the search query. For example, if I search for ["the sum of two odd numbers is even"](https://www.moogle.ai/search/raw?q=the%20sum%20of%20two%20odd%20numbers%20is%20even), I turn up the result `Odd.add_odd` which matches this description pretty well as the fourth result. |
There was a problem hiding this comment.
In my opinion, "semantic search" is not quite an accurate description. Maybe "LLM-based search"?
|
|
||
| [Loogle](https://loogle.lean-lang.org/) is a third search engine for mathlib developed by Joachim Breitner at the [Lean Focused Research Organization](https://lean-fro.org/). It is meant to be a similar tool to [Hoogle](https://hoogle.haskell.org/) from the Haskell community: It allows you to search for lemmas by their type signature. For example, if I search for [`(?a -> ?b) -> List ?a -> List ?b`](https://loogle.lean-lang.org/?q=(?a%20-%3E%20?b)%20-%3E%20List%20?a%20-%3E%20List%20?b), I get results for `List.map`. | ||
|
|
||
| Loogle is a great tool for finding lemmas that you know the type of, but not the name of. It is a pretty precise tool; a downside is that it will not by default give you responses without you typing out the names of the definitions relevant to your search correctly and in full. To avoid putting in too many restrictions and getting an empty result list, it's recommended that you add search filters one at a time to your query. |
There was a problem hiding this comment.
I personally tend to use it more with just a list of definitions that are used rather than a full type signature. Maybe "...by their type signature or types that occur in it"
|
|
||
| ### Zulip | ||
|
|
||
| The [Zulip chat](https://leanprover.zulipchat.com/) for the Lean community has a channel called ["Is there code for X?"](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F) where you can ask questions about the presence of particular theorems in mathlib, major and minor. If you are having trouble finding a theorem, you can ask in this channel and someone will likely be able to help you, although it might take longer than the search engine would. |
There was a problem hiding this comment.
Perhaps add "You can also search the archives to see if someone has asked about the same results before."
kbuzzard
reviewed
Dec 8, 2024
| ## Other websites | ||
|
|
||
| There are a few other websites that can be helpful for finding theorems in mathlib, although they are not conventional search engines like the ones above. | ||
|
|
There was a problem hiding this comment.
I think that leansearch.net should be mentioned.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a blog post I wrote detailing a variety of ways a beginner might search for theorems in mathlib.
Inspired by @j-loreaux 's video on the subject, and this thread. I have tried to make it pretty open-minded and comprehensive, I am happy to take suggestions if there are strategies I missed.