The project remains focused on logic-based tools to support programming and on
implementing formal computational mathematics; we see these as inextricably
linked activities. Over the years the scope of the project has expanded - from
developing individual programs and theorems to constructing systems and theories. Starting
with the slogan "proofs-as-programs," we now talk about
"theories-as-systems." This change of scale has led to a new class of problems
and challenges discussed throughout this project summary.
Build proof assistants that are as indispensible to programmers and mathematicians as
word processors are now.
Design and implement proof assistants that consistently exhibit problem solving behavior
considered "intelligent" - in the sense that Deep Blue is an
"intelligent" chess player.
Create consistent standard formalizations of the core mathematics that are widely
assumed as background in computing and mathematics education at the college level and that
are frequently used in designing algorithms and systems.
Provide convenient access to the digital libraries of formalized mathematics mentioned
just above that is so useful that the formal material becomes a standard reference for
mathematical knowledge and is widely cited in textbooks.
Technical Content and Cross Links
The project is multi-faceted. One way to understand it is to see its projections onto
other areas of computer science and mathematics. The standard projections are onto these
topics:
