Experiments and Results of FDL (30+discussion)

As the amount of online formal mathematical content grows, for example through active efforts such as Logosphere, Mathweb, Cornell's Formal Digital Library (FDL), and others, it becomes increasingly valuable to find automated means to manage this data and capture semantics such as relatedness and significance. In this talk, I discuss results from applying graph-based approaches, such as HITS, or Hyperlink-Induced Topic Selection, used for World Wide Web document search and analysis, to formal mathematical data collections. The nodes of the graphs analyzed are theorems and definitions, and the links are logical dependencies. By exploiting this link structure, I show how one may extract organizational and relatedness information from a collection of digital formal math. This work was done in collaboration with Jon Kleinberg, Robert Constable, and Richard Eaton.