It's August 2024. To say the "theorem search in Lean" ecosystem is thriving is an understatement, last time I used Lean (less than a year ago?) most of these tools didn't exist.
July 24th 2024 Kevin Buzzard was giving the "The state of the art in the formalisation of research-level mathematics" talk during the "Interactive Theorem Proving in Education and Research" workshop (link).
During the questions section, I asked something along the lines of "what do mathematicians use for searching theorems in Lean lately - Loogle, Moogle, ReProver, #find tactic, something else completely?".
Kevin Buzzard responded with something along the lines of "Moogle! Once there was a 6-hour Moogle outage, and that was the only thing zulip discussed".
So - let's start from listing all of our options, perhaps with a mild bias towards Moogle.
NOTE - this is very much WIP, but already explorable.
UPDATE - this became even more WIP. Still explorable though.
First of all, an overview.
While traditional search engines only begin to experiment with semantic search (say, nn-first approach of exa.ai), Lean theorem search seems to be overpowered by nn-first approaches.
Both Moogle.ai and LeanSearch.net support a formal pattern-matching approach apart from their main nn-based search entry.
Throughout this post, we'll be searching for a simple theorem - not_exists from Mathlib.
theorem not_exists {α : Sort u_1} {p : α → Prop} :
(¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x
Neural search engines will be queried with ¬∃ (x : α), p x then ∀ (x : α), ¬p x
,
formal search engines will be queried with (¬∃ (x : α), p x) → ∀ (x : α), ¬p x
.
In no way is this the best possible testing query - my goal for this post is to showcase the interfaces of these systems for a theorem that everyone can understand.
What we mean by "neural" here is a vector search engine.
With all such search engines, you have to perform the same dance:
d ^ m < d ^ n * d * 25 - d ^ n * 4
, and you want to turn it into a hypothesis with type d ^ m < d ^ (1 + n) * 25 - d ^ n * 4
.Nat
s into Real
s), dealing with associativity/commutativity, and, finally, matching hypotheses to arguments.Link | Authors | Announcement |
https://leansearch.net | Jiang Jiedong, Guoxiong Gao, Haocheng Ju | Zulip, 30th July 2024 |
LeanSearch is a semantic search engine.
Long story short - per each theorem in Mathlib, it takes a mathlib formal statement and its context (docstring, related definitions, etc.), and "informalizaes" it using GPT-3 - turns the theorem statement into a natural language description.
Then, it creates the semantic embedding [theorem name; theorem's formal statement in Lean; natural language version of this theorem] and puts it into the vector database (one vector == one theorem; theorems are considered similar when the cosine distance between these two vectors is small).
When searching for theorem in the LeanSearch interface, the user can type anything they like - LaTeX formulas, approximate theorem name, term descriptions, natural language queries - LeanSearch can digest all of it.
Anecdotally, if you input something obviously silly like theorem name that has many letters "z"
, semantic search will happily return theorem List.zip_unzip
. If you input theorem that they learn in school
, semantic search will happily return theorem Nat.sq_sub_sq (a : ℕ) (b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b)
.
After the query is submitted, the query text undergoes query augmentation using GPT-4 (something along the lines of "You're a maths expert, please transform this lousy query into proper maths speak AND accompanying Lean 4 code"). [Update - in the real LeanSearch.net, the query augmentation is not automatic at the moment - you have to press a button in their interface to perform it]
After this process, we have vectors representing all theorems in Mathlib, and a vector representing our augmented search query. Using cosine similarity, we find the theorem vectors that are most similar to the query. Those are our search results.
MY USE
I use it all the time.
Link | Authors | Announcement |
https://moogle.ai | The Morph Labs | Zulip, November 2023 |
Moogle is a hybrid. In order to perform a formal pattern-matching search, start your query with #find
.
Unlike LeanSearch.net, Moogle is yet to publish a paper about their system.
It's unclear whether LeanSearch.net or Moogle.ai performs better, both are worth trying. LeanSearch.net paper claims performance superior to Moogle.ai's, and I personally prefer LeanSearch.net for daily use.
As mentioned in the introduction, Moogle seems to be the most popular search engine at the moment - probably because it was the first semantic search engine for Lean. At the moment of writing, LeanSearch.net is one-month-old.
MY USE
I have a preference for LeanSearch.net at the moment.
Link | Authors | Announcement |
huggingface.co/spaces/dx2102/search-mathlib | Deming Xu | Zulip, 30th July 2024 |
Published, quite unfortunately, on the same day as LeanSearch.net - this is a simple model on huggingface. Returns pretty good results, but this was merely a training exercise for the author as he states in his introduction on zulip.
I think the zulip message by Deming Xu is worth a read - with only 100 lines of Lean code (adjusted code taken from another library) + 200 lines of Python code (100 of which is just setting up the web page), he managed to create a search engine that performs reasonably well, which is quite inspiring to anyone who wants to experiment with semantic search in Lean 4.
The principles are similar to what LeanSearch.net (and, likely, Moogle) is doing - convert all theorems into vectors, convert a search query into a vector, put all of these vectors into vector database, and determine the theorem vectors closest to the search query vector. The main difference between LeanSearch.net and Deming's huggingface model is that LeanSearch.net enhances both the theorem vectors and the query vector using conversion to natural language - Deming just uses raw Lean data (theorem name, theorem type, theorem docstring).
MY USE
I don't use it (and it was never intended for use!), as there exist LeanSearch.net and Moogle.
#find
)Link | Authors | Announcement |
https://loogle.lean-lang.org | Joachim Breitner | Zulip |
Loogle was developed by Joachim Breitner, and was reportedly (link) inspired by Haskell's Hoogle.
Loogle's search is not semantic, it matches expressions by their exact structure. Technically, Loogle is a wrapper around Mathlib's #find
- it adds some functionality to the default #find
command, and creates a web interface around it.
Initially, Joachim tried to merge two #find
PRs (#6643 and #6363) into Mathlib 4, but the reviews went for too long, so he just went ahead and:
1) factored out #find + batteries
into a separate repo (https://github.com/nomeata/loogle), and
2) created https://loogle.lean-lang.org, which uses this #find + batteries
internally.
MY USE
I started using Loogle from within its vscode interface recently, I love it so far. At the moment I use it about as frequently as I use leansearch.net.
apply?
and exact?
(aka library_search
)From the docs:
library_search
has been renamed toapply?
(orexact?
if you only want solutions closing the goal)
Both apply?
and exact?
work on a goal only.apply?
will find all theorems that are legal to execute on a goal.exact?
will find all theorems that are legal to execute on a goal, AND that do close the goal.
Here is the interface for the apply?
tactic:
Good docs: https://lean-lang.org/blog/2024-4-4-lean-470/.
MY USE
I useexact?
regularly, and do not useapply?
at all.exact?
is wonderful, but something to keep in mind is 1) it won't find anything if some additional hypothesis is lacking, so always do the preliminaryhave h : 2 > 0 := by positivity
in your context! 2) it won't deal with casting, make sure all of your hypothesis and the goal are cast appropriately before callingexact?
.
Link | Authors | Announcement |
https://github.com/lean-dojo/LeanCopilot (install as a Lean library) | Kaiyu Yang, others | Zulip, |
Unlike the search engines above, Lean Copilot takes inspiration from GitHub Copilot - it looks at the current state of your proof, and tries to predict the next useful step.
Lean Copilot can be considered a search engine because, using the select_premises
tactic, you can search "relevant theorems to my proof" with it (confusingly enough, when they say "premises"
- they mean "theorems"
). It will look something like this (image courtesy of LeanCopilot repo):
MY USE
I couldn't install it on my mac due to the known issue.
Something not immediately obvious is that powerhouse tactics such as linarith/omega/ring/simp/simp_all/aesop is also, practically, search.
The idea is that you see what your goal is like, and you have a hunch for whether one of these tactics would solve it. For example, if you have a set of inequalities, and you want to prove an inequality, and all of them are simple enough, the linarith should succeed. If not, try to make the inequalities in question even more simple, and repeat the linarith attempt.
Right now I'm going by such hunches, but I do kind of wish there was a flowchart for when exactly to try each such tactic, and what other such tactics are available.
Usage of llms is also a search. Large language models, such as ChatGPT and Claude were mainly rained on Lean 3 and older Mathlib versions, but they understand the fundamentals of proof assistants just fine. Their inexperience with Lean 4 is easily circumvented by pasting relevant theorems into your prompt.
Claude is much better than ChatGPT in proof writing at the moment.