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.