How to use LeanSearch from VSCode?

Stream: general

[Vasily Ilin]

https://github.com/leanprover-community/LeanSearchClient?tab=readme-ov-file shows examples like #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
when I put it in my VSCode, I get unexpected token '#'; expected command. When I use leansearch instead of search, I get Could not contact LeanSearch server.

[Chris Birkbeck]

I've got the same problem, I keep getting the could not contact LeanSearch server error. Edit: although #loogle does work.

[Junyan Xu]

import Mathlib
#search "If a natural number n is less than m, then the successor of n is less than the successor of m."

says "Could not contact LeanSearch server". Maybe #search needs more imports?

[Siddhartha Gadgil]

@Chris Birkbeck and @Junyan Xu does #leansearch work but not #search at the same time? Otherwise it is likely to be just the LeanSearch server having gone down, or at least its API (I tested just now and got the same error).

@Vasily Ilin You may have an older Mathlib, so an older version of LeanSearchClient.

[Siddhartha Gadgil]

I should check though if LeanSearch has changed its API.

[Chris Birkbeck]

#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

also gives me the same error

[Junyan Xu]

Sorry I forgot to say I was testing in the web editor.

[Siddhartha Gadgil]

Looks like they changed the API, so my announcement was unfortunately timed. Testing now to fix.

[Siddhartha Gadgil]

It seems that the changes are quite a bit. I will fix the LeanSearchClient but it is getting late here, so it will have to wait till the morning.

[Siddhartha Gadgil]

The fix has been pushed, but will take some time to make it to Mathlib (and not 4.18.0 unfortunately). I will also test it better before updating.

[Vasily Ilin]

Thank you! I'll try it tomorrow

[Kim Morrison]

@Siddhartha Gadgil I'm currently see two problems with #search. On current Mathlib master, typing:

#search "Lemmas about the counts of elements in lists under permutation."

I get two info messages --- one of which is the raw JSON returned. This needs to be turned off!

But secondly, in the infoview, I get

Suggestions
LeanSearch Search Results
#check List.subperm_iff_count -- ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α], l₁.Subperm l₂ ↔ ∀ (a : α), List.count a l₁ ≤ List.count a l₂
See also `List.subperm_ext_iff`.
#check List.perm_replicate_append_replicate -- ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a b : α} {m n : ℕ},
  a ≠ b → (l.Perm (List.replicate m a ++ List.replicate n b) ↔ List.count a l = m ∧ List.count b l = n ∧ l ⊆ [a, b])
#check length_permsOfList -- ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), (permsOfList l).length = l.length.factorial
#check Multiset.powersetCardAux_perm -- ∀ {α : Type u_1} {n : ℕ} {l₁ l₂ : List α},
  l₁.Perm l₂ → (Multiset.powersetCardAux n l₁).Perm (Multiset.powersetCardAux n l₂)
#check List.length_permutations -- ∀ {α : Type u_1} (l : List α), l.permutations.length = l.length.factorial
#check List.count_permutations'Aux_self -- ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α),
  List.count (x :: l) (List.permutations'Aux x l) = (List.takeWhile (fun x_1 => decide (x = x_1)) l).length + 1

while in the "Problems" tab I just see

LeanSearch Search Results
• #check List.subperm_iff_count
• #check List.perm_replicate_append_replicate
• #check length_permsOfList
• #check Multiset.powersetCardAux_perm
• #check List.length_permutations
• #check List.count_permutations'Aux_self

It would be really great if the comments could also appear in the problems tab --- I've been experimenting with getting AI agents (e.g. cursor) to use #search when they need help finding theorems, and such agents can be instructed to read the problems view (it helps to call it "linter output", even though that's not normal Lean nomenclature!), but they can't read the InfoView.

[Siddhartha Gadgil]

I will work on both these

[Vasily Ilin]

@Kim Morrison , will you share the results of your experiments with the agents? I think it would be very valuable. E.g. what is the setup, what is the prompt, what kind of results you get? Thank you!

[Oliver Dressler]

Kim Morrison said:

I've been experimenting with getting AI agents (e.g. cursor) to use #search when they need help finding theorems, and such agents can be instructed to read the problems view (it helps to call it "linter output", even though that's not normal Lean nomenclature!), but they can't read the InfoView.

If you are not opposed to using an MCP, I have added a tool to make leansearch available to an agent in lean-lsp-mcp (via the API). Interestingly I found that the raw response can be well interpreted by the agent.

If used in VSCode you can additionally toggle which tools the agent is allowed to use. However, in Cursor this is not feasible yet, so the agent will automatically get access to all other tools in the MCP beside leansearch as well.

[Kim Morrison]

@Oliver Dressler how essential is the python in your setup? (I have an aversion to investing time in tools which couldn't be used widely by the Mathlib community, because ... that's my job. :-)

[Oliver Dressler]

Yes, I understand! The Python in this setup is currently used in:

• The MCP server (based on the python-sdk). This could also be implemented in another language. The MCP server communicates with the agent using JSON-RPC 2.0 via stdio or HTTP. In Lean, the built-in language server already uses this communication protocol. E.g. The above mentioned leansearch functionality could easily be translated to another language.
• The package manager (uv) allows for easy installation of the MCP server in an IDE. This functionality is not essential, so could be left out.
• Many tools in this MCP are based on the LSP; E.g. getting goals, term goals or hover information at a specific position. Here I use leanclient, which is Python-based. Replacing this part with another language would require a Lean LSP integration or implementation in Lean.

Overall none of these are exclusive to Python, but they are convenient.
An MCP based on a VSCode extension could be a viable alternative, as it provides all above mentioned functionality.

[Johan Commelin]

Wouldn't that make it harder to use it in headless mode? Or in conjunction with nvim?

[Siddhartha Gadgil]

A pure Lean program would work everywhere. The main barrier I find personally is a lack of an http server and client (for the client we can just use curl in practice).

[Oliver Dressler]

Johan Commelin said:

Wouldn't that make it harder to use it in headless mode? Or in conjunction with nvim?

Yes an implementation as a VS Code extension would become exclusive to VS Code and Cursor (based on VS Code).

[GasStationManager]

It would be great when/if someone implements a lean SDK for MCP. Meanwhile, MCP's lack of Lean support shouldn't be a barrier...
Besides LeanSearch, many Lean features can be very useful to the AI agent, and exposing the functionality as MCP servers makes it available in a wide range of settings. In that sense, implementing a MCP server using one of its existing SDK languages is no different than when you need to write some javascript to implement a VS Code extension.

From the users' point of view, my hope is that apps that are serious about MCP adoption will soon ship prepackaged with the python and typescript SDKs for MCP, so that users wouldn't have to install python manually.

[Kim Morrison]

Vasily Ilin said:

Kim Morrison , will you share the results of your experiments with the agents? I think it would be very valuable. E.g. what is the setup, what is the prompt, what kind of results you get? Thank you!

I was interested to see what can be done "out of the box", i.e. with no additional software installed. First, I needed a hack, to convert all info and warning messages into errors, as otherwise Cursor can't see them [1]. With that out the way, the following prompt

You can use #moogle "infinitely many primes" to query for relevant lemmas using a natural langauge query. The results will be returned as linter messages. Write this at the end of the source code of this file, and then read the resulting linter messages. This will suggest some lemma names. You can then write #check lemma_name for any interesting ones, and again read the linter messages. Finally, tell me the most relevant theorem, and what it says.

successfully induces the cursor agent to try running

#moogle "infinitely many primes"

then retry with

#moogle "infinitely many primes."

then read the results and write

#moogle "infinitely many primes."
#check Nat.Primes.infinite

before finally telling me:

Based on the linter messages, the most relevant theorem is Nat.Primes.infinite, which states that the set of prime numbers is infinite. This is a fundamental result in number theory, often attributed to Euclid, which proves that there are infinitely many prime numbers.

The theorem is stated in Lean as Nat.Primes.infinite : Infinite Nat.Primes, where Nat.Primes represents the set of prime numbers and Infinite is a type class that indicates the set has infinitely many elements.

This is one of the most important theorems in mathematics, and it's interesting to see it formalized in Lean. The theorem is particularly significant because:

1. It's one of the oldest known mathematical proofs
2. It's a fundamental result in number theory
3. It has many important consequences in mathematics
4. It's a great example of a proof by contradiction

Would you like me to explore any of the other related theorems that were found in the search, such as Nat.exists_infinite_primes or Nat.infinite_setOf_prime_modEq_one?

That seems essentially perfect?

[Kim Morrison]

(except, I guess, its editorializing "one of the most important theorems in mathematics" ... :-)

[Kim Morrison]

It's seems fairly reliable, e.g.

Next, use the same technique to try to locate the statement that for metric spaces, sequential compactness and compactness are equivalent.

reports back

UniformSpace.isCompact_iff_isSeqCompact.{u_1} {X : Type u_1} [UniformSpace X] {s : Set X}
[(uniformity X).IsCountablyGenerated] : IsCompact s ↔ IsSeqCompact s

[Kim Morrison]

Not exactly what I asked for, I guess.

[Vasily Ilin]

@Siddhartha Gadgil , the error I experienced is still there.

example (a b : ℝ) (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
  #leansearch "log."

gives Could not contact LeanSearch server.
This is on 4.18.0. Should I be trying on a different version? Which one?

[Siddhartha Gadgil]

The upgrade will take effect on 4.19.0-rc3