a search engine for Isabelle

Stream: Machine Learning for Theorem Proving

[Jeremy Avigad]

The following announcement, recently posted on the Isabelle Zulip group, may be of interest to some here:

The ALEXANDRIA project is excited to announce the release of the SErAPIS concept-oriented search engine for the Isabelle libraries and AFP 2021.

Homepage: https://behemoth.cl.cam.ac.uk/search/
User Guide: https://behemoth.cl.cam.ac.uk/search/SErAPIS_online_user_guide.pdf

SErAPIS (Search Engine by the ALEXANDRIA Project for ISabelle) is an experimental search engine for Isabelle designed to allow Isabelle users to search and explore the libraries and AFP using keywords and mathematical concepts (natural language phrases that refer to mathematical objects and ideas).

We invite you to try it out. For tips on how to construct effective queries, please see Section 3 of the user guide.
Note that there are 6 different methods to experiment with.

SErAPIS is also a platform for conducting research in novel methods to search Isabelle collections and machine learning in Isabelle.

We kindly ask that you help us with our research by providing us with feedback on the relevance of SErAPIS search results to your searches.
Giving us feedback is optional but very easy to do (see Section 4 of the user guide).

Your feedback will help us:

(i) build data-sets for Isabelle search and machine learning,
(ii) develop new search algorithms for Isabelle collections and;
(iii) develop machine learning methods for aiding the construction of proofs in Isabelle.

All data collected is anonymised.

Thank you,

Yiannos Stathopoulos @Yiannos and Angeliki Koutsoukou-Argyraki.