The MathWebSearch system (MWS) is a content-based search engine for mathematical formulae. It indexes MathML formulae, using a technique derived from automated theorem proving: Substitution Tree Indexing. With this indexing technique MWS can answer unification queries extremely efficiently (30-100 ms) on large sets of formulae (in the Gigaformula range); but the index (up to 50GiB) needs to be kept in main memory.

MWS is the formula search engine employed in Zentralblatt Math; see a demo on a mathematical subset of the arXMLiv data set further demos.

The MathWebSearch system is Open Source, developed on GitHub, and is (by now) easily deployable via a set of docker containers. We can give your project a search interface like the nLab search for nLab at the cost of theming the user interface and building a harvester.