PRL Seminars
Steps Toward a World Wide Digital Library
of Formal Algorithmic Knowledge
Abstract
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.
|