What is this?

ProofDB is a natural language search engine for querying a large corpus of theorems in Coq.

Which theorems, specifically?

Currently, ProofDB queries theorems defined in an installation of the community beloved Coq Platform. This includes many developments beyond the standard library, such as mathcomp.

How do I use this?

This is a research preview of ProofDB, and we're still figuring out the interface and best practices. Here are some typically effective searching strategies, though:

• Search for topics you'd like lemmas about in concise plain english, e.g. "matrix transpose" or "group inverse"
• Search for lemmas symbolically: due to the composition of the training data for the search engine, ProofDB can make use of common notations as hints to find relevant theorems, e.g. "a+b=b+a" or "a*a^-1=1"
• A combination of the above.

This is still a work in progress, so the most "relevant" theorem might not be the first one!

I'm getting results that seem relevant but for strange/niche types.

You can make use of filters (explained below) to limit results to theorems that operate on the types you're working with. Alternatively, we try to offer automatic "search refining" questions when possible. Answering these to the best of your knowledge will iteratively refine the search to relevant libraries and types.

ProofDB by default uses a fuzzy neural search to find relevant theorems. This is helpful when you're not sure exactly what you're looking for. However, the neural search can be frustrating when you DO know very specific things about the theorem you're searching for.

To complement ProofDB's fuzzy functionality we offer a set of filters that restrict the search results to those that satisfy a particular predicate. The syntax for a filter is `{filter_name}:"{filter_argument}"` appended to the end of a search. Any filter's behavior can be negated by prefixing the filter name with a '-'. You can use as many filters as you want and all will be conjunctively applied to the search results.

What follows is a list of defined filters:

• The in filter filters the results to theorems whose location is prefixed with the filter's argument. For instance, in:"Coq" will cause a search to only show results from within the Coq standard library.
• The arg filter filters the results to theorems that have at least one of a particular argument. For instance, arg:"nat" will cause a search to only show results that take a natural number as an argument. Warning: due to the semantics of Coq modules and imports, some types may have a module prefix that typically does not appear in normal environments. If in doubt, this filter supports wildcards to match against arbitrary prefixes, suffixes, and infixes in arguments. arg:"*Q*" will match any result with an argument that contains a Q.