The working mathematician is confronted often with a new model or a new theory whose connections with other parts of mathematics are not known.
The goal of this project is to produce one Library of models, axiomatics and results that in the end will allow any mathematician to automatically find the connections to pats of the literature  of his model or of his brand new theory.
We use automated reasoning to carry this task out.