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.

Maybe you want to add this to https://isabelle.systems ? You can add an entry here https://github.com/isabelle-prover/isabelle-prover.github.io :)

Is it o.k. if I post this to the Lean Zulip group? I am guessing that many in the community there will be happy to experiment with this.

Sure, please do @Jeremy Avigad --and many thanks for the interest! We would be most grateful for user feedback-- the more feedback the better! Thank you again!

I’d like to point out that:

Methods 1,2,3, 5 and 6 are concept-oriented: they use the input concepts very differently. If one method (default is method 2) is not producing good results in response to the concepts you input, another method might!

NB: The last indexing of the Archive of Formal Proofs was done on 23/2/2021, so AFP entries after that date are not included. We will be re-indexing every now and then so as to be as up-to-date as possible!

Many thanks for the suggestion @Kevin Kappelmann , I just created a pull request--hope it looks ok!

Done!

That's a cool project!

I would like to point out a (minor) naming collision, however: https://github.com/ejgallego/coq-serapi

I'm not sure how much of an issue it really is, since the SerAPI project is so far still fairly unknown/small (and lives in the disjoint Coq universe anyway), but I wanted to mention it.

Thank you for letting us know @Max Kirchmeier . We weren't aware of this--luckily the names are not the same, though very similar. Hopefully there won't be any confusion as the Coq project is not a search engine. In our case, SErAPIS stands for "Search Engine by the Alexandria Project for ISabelle" and it is an intended pun referring to the deity "Serapis" (see e.g. wiki) once worshipped in Alexandria--which is the name of our ERC project--inspired by the Library of Alexandria in Egypt, since we are working with libraries of formal proofs :) https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/

Last updated: Dec 07 2023 at 16:21 UTC