Finding and Presenting Alignments in Math Libraries
We importer formal and informal libraries of mathematics into the MathHub system. The formal libraries are mostly theorem prover libraries (Mizar, HOL Light, Isabelle, IMPS, PVS, ... ) and the informal ones are based on annotated LaTeX.
We observe that there is quite a lot of overlap between the libraries, and we have developed a notion of "alignments" (see a recent paper and have collected an initial set.
This general topic has various sub-projects that can be tackled individually or together
- building an alignment navigator/interface, which allows users to get an overview over the overlap and how concepts relate (Akbar Oripov is working on this at Jacobs University).
- manually finding complex alignments and categorizing them, and building a curation system for that.
- building software that goes over the libraries and suggests alignments of various categories (to be curated in the system above).