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.

Proposal Summary

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:

  • a workshop to collect ideas, achieve necessary consensus, and formulate a plan of action,
  • travel to facilitate collaboration by the initial set of principal implementors, and
  • dissemination of the concept and initial results in order to attract more participants.
    • The complete proposal is available here.