Working for nearly a century, mathematicians, logicians and computer scientists have achieved the practical means to formalize and mechanically verify vast amounts of mathematical knowledge. That formal knowledge and the tools used to create it have become valuable in the task of improving the reliability of software and our ability to program it more efficiently.

Storing this formal material on-line in digital libraries will make it more valuable. This talk discusses the Formal Digital Library being designed and built at Cornell, Cal Tech and Wyoming with support from an ONR URI grant.