Project Focus and Goals

    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.

    We are currently focused on these goals:

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. The state of affairs we are striving for is one in which: proof assistants are full partners in solving major open mathematics problems such as P = NP?; proof assistants fill in or instantly recognize inference steps that are considered obvious by well educated users, and they also routinely "discover" unexpected solutions to problems;

Our strategy to achieve this "intelligent behavior" is to include the best problem solving heuristics; make them fast; and integrate them with the symbolic algorithms and data bases of mathematical knowledge.

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;

standard data structures and algorithms - numerical, symbolic, algebraic, geometric, logical, etc.; the mathematical semantics of programming languages, reactive systems, problems solving environments, etc.; mathematical models of physical systems and social systems (economies, populations).

Our strategy for this task is to use the most expressive formalism consistent with our goals. A key requirement is that the logical theory is able to express computational ideas and distinctions. Our priority has been to provide maximal expressiveness and then figure out how to automate it well.

Provide convenient access to the digital libraries of formalized mathematics; access that is so useful that the formal material becomes a standard reference for mathematical knowledge and is widely cited in textbooks. This will entail:

writing definitions, claims, theorems and proofs that are easy to read and understand; enabling major theorem provers to share libraries of mathematics so that a large amount of material can be accumulated and indexed; providing extensive cross-linking and indexing of the formal material, including connections to informal text.