Rocq Lemmas Search
I develop a website (https://lemmasearch.com/) for searching theorems in the projects of the Rocq Platform.
I modify the Rocq compiler to extract theorems and their dependencies (functions and types), totalling 77,753 theorems and 45,196 definitions. For retrieval, I use the BM25 algorithm. There are better options out there — embedding-based models like RocqStar Ranker Embedder or LLM-based agents would likely give more accurate results — but the server (2 vCPUs, 4 GB RAM, no GPU) makes that impractical for now.
The goal of the site is to make searching for theorems and definitions more convenient. Since BM25 computes similarity based on text, you just need to describe what you’re looking for in plain language — no need to recall the exact Rocq syntax. The site also supports searching across multiple projects at once, so you don’t have to search through each project one by one.
The website is still under development. If you have any suggestions, would like a specific project to be added, or notice any missing theorems or definitions, feel free to contact me via email.
Project Selection
Currently, the site covers theorems and definitions from projects in Rocq Platform 2025.08.2 (Rocq 9.0.1) and 2025.01.0 (Rocq 8.20). https://lemmasearch.com/ always points to the latest Rocq Platform distribution. If you need to search projects from Rocq Platform 2025.01.0 (Rocq 8.20), use https://lemmasearch.com/820 instead.
Lemma Search
On the left side of the search bar, we can choose which project to search in. By default, the site searches for theorems. “All” means searching across all current projects.
For example, suppose we want to find theorems about the rev operation on lists, and we expect the theorem to involve the append operator ++. We can enter the keywords list rev ++ into the search bar. The BM25 algorithm will rank theorems whose statements or names contain these terms highly, making it easy to locate relevant results such as rev_length or lemmas about how rev interacts with ++. Clicking “Details” on a search result will show the definitions and inductive types that the theorem depends on.
Definition Search
The site also supports searching for definitions (function definition or inductive type). To use this feature, check the “Definition” option next to the search bar, then enter keywords related to the definition you are looking for. For example, entering compare x y will surface definitions whose names or bodies contain those terms.
Pattern Matching
Currently, the search supports a simple pattern matching. Use pattern:rule. to specify a rule (note: there must be a dot at the end!). The current pattern match is implemented using regular expressions; the rule between pattern: and . will be converted into a regular expression.
As shown in the figure below, the query length pattern:_ ++ _ = _ ++ _. specifies that the lemma must contain a subterm of the form _ ++ _ = _ ++ _ and be related to length. The search engine first filters the theorems whose statements match the pattern _ ++ _ = _ ++ _, and then uses the BM25 algorithm to rank the remaining results by the keyword length. The pattern syntax is similar to that of the Search command in Rocq, where _ serves as a wildcard matching any term.
Share Search Result
The current search result can be shared directly via its URL. The URL encodes both the selected project and the query, so anyone opening the link will see the same results. For example, the URL for the query list rev ++ across all projects is:
https://lemmasearch.com/?project=All&query=list+rev+%2B%2B
Sharing this link allows others to immediately view the same search results without having to re-enter the query manually. The URL-encoded format also makes it straightforward to integrate with LLM agents or other tools — a query can be constructed programmatically and passed directly as a URL to retrieve relevant theorems or definitions.
Update on July 26, 2025
Most projects on the Rocq platform have been added to the search.
Update on October 27, 2025
Added the search for definitions. Now you can check the “Definition” option to search for the definition of objects in each project.
Update on October 29, 2025
Add type information of definitions.
Update on November 3, 2025
Add two projects: coq-fcsl-pcm and coq-htt.
Fix some bugs.
Update on December 15, 2025
Fixed bugs: different queries return the same results.
Update on April 17, 2026
Rewrite the tutorial documentation for the site. Added projects from the latest Rocq Platform distribution (2025.08.2) to the search database.
— Jun 19, 2025