FindFacts: A Scalable Theorem Search

TL;DR

FindFacts is a scalable, domain-specific search tool for Isabelle formal proofs that enables efficient interactive searches across the entire AFP without relying on term unification.

Contribution

It introduces a novel, scalable search engine for Isabelle theories, improving over existing tools by enabling comprehensive, interactive searches of the entire AFP.

Findings

Supports interactive search of over 500 articles in AFP

Uses a classical drill-down search engine instead of term unification

Enables scalable search across the entire Isabelle archive

Abstract

The Isabelle Archive of Formal Proofs (AFP) has grown to over 500 articles in late 2019. Meanwhile, finding formalizations in it has not exactly become easier. At the time of writing, the site-specific AFP google search and the Isabelle find_theories resp. find_consts commands (that only work on imported theories) are still the only tools readily available to find formalizations in Isabelle. We present FindFacts, a novel domain-specific search tool for formal Isabelle theory content. Instead of utilizing term unification, we solve the problem with a classical drill-down search engine. We put special emphasis on scalability of the search system, so that the whole AFP can be searched interactively.