Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge

by Robert L. Constable
2003-2004

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.

Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge

by Robert L. Constable 2003-2004

by Robert L. Constable
2003-2004