Algorithmic Software Verification Project Proposal
QED Project Summary
The aim of the QED project is to build a single, distributed, computerized
repository that rigorously represents all important, established mathematical
knowledge. The construction of this system will be a scientific undertaking
of significant proportions, requiring the cooperation of many mathematicians,
computer scientists, research groups, research agencies, universities, and
corporations. This system will have benefits for mathematics, science,
technology, and education.
This proposal was for first-year funding to start the QED Project to formalize
and verify a significant body of mainstream mathematics. The basic activities
to be funded were:
The complete proposal is available here.