Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge
by Robert L. Constable
Our work involves building and experimenting with a digital library of machine checked mathematics; we call such mathematics formal.
The appeal of the research agenda for this field is that computers help us create knowledge and accelerate discovery by processing the information on which knowledge is based. Computers reveal patterns invisible to an unaided mind; they can check claims against vast collections.