Improving searching in docs

Stream: general

[Praneeth Kolichala]

The search feature seems to not take into account theorem descriptions (compared to the mathlib 3 version of the documentation which did).

Example:

Searching for "pigeonhole principle" gives this, a bunch of completely irrelevant results, but used to give the correct result (fintype.exists_ne_map_eq_of_card_lt) as the 5th search result (the other results were all reasonable -- two measure theory versions of the pigeonhole principle, two infinite versions).

The new search also seems to freeze/lag more frequently when typing. Perhaps the UI experience could be improved using webworkers or something if available (or simply improving the search speed)?

Finally, a request: it would be really wonderful to have a fuzzy type-based search. Given these assumptions and this result, can you find a theorem that uses most of the assumptions and gives something close to the result? This could be a tactic or part of the web-based documentation search. It would be similar to library_search but I don't want to have to specify the requirements exactly, and the resulting expression does not necessarily have to typecheck.

[Junyan Xu]

Seconded. For fuzzy search you might try LLM-based Mathlib semantic search or Wolfia (generic repo search, discussion thread)