A search engine for mathematical formulae

Abstract. We present a search engine for mathematical formulae. The MathWebSearch system harvests the web for content representations (currently MathML andOpenMath) of formulae and indexes them with substitution tree indexing, a technique originally developed for access-ing intermediate results in automated theorem provers. For querying, we present a generic language extension approach that allows constructing queries by minimally annotating existing representations. First experi-ments show that this architecture results in a scalable application.