A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics

unofficial copies [PDF], [PS]

by Lorigo, L. , Kleinberg, J., Eaton, R., Constable, R.

International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science, Springer-Verlag, Vol 3119, pp. 220-235, 2004.

Re-released as Technical Reoprt, Cornell University TR2006-2015, 2006.


As the amount of online formal mathematical content grows, for
example through active efforts such as the Mathweb [21], MOWGLI [4],
Formal Digital Library, or FDL [1], and others, it becomes increasingly
valuable to find automated means to manage this data and capture semantics
such as relatedness and significance. We apply graph-based approaches, such
as HITS, or Hyperlink-Induced Topic Search, [11] used for World Wide Web
document search and analysis, to formal mathematical data collections. The
nodes of the graphs we analyze are theorems and definitions, and the links are
logical dependencies. By exploiting this link structure, we show how one may
extract organizational and relatedness information from a collection of digital
formal math. We discuss the value of the information we can extract, yielding
potential applications in math search tools, theorem proving, and education.