The preceding section on accomplishments should make clear that much has occurred in the field of automated deduction and that the activity level is high. But also much remains to be done, and in this section we address the question of what can be done in the near-term and in the longer view. There should be no question of the worth of continuing this research. For example, both VLSI chips and networks are increasing in complexity, and the need to verify that these systems function as intended is growing proportionally. This is made vivid by the Pentium incident and reinforced by the examples of the preceding section. (The Pentium microprocessor had a faulty floating-point divide implementation that ultimately cost the manufacturer millions of dollars with the recall of hundreds of thousands of chips.) Thus, there is considerable economic incentive pushing the continued research in this area. Besides economic forces, social and intellectual forces also drive research directions and investment. Our social role is in education, mathematics primarily, but certainly parts of computer science and other subjects as well. There is also a clear intellectual role centered on mathematics: the solution of open problems and, eventually, the development of new mathematics. At the end of this section we argue that the intellectual role actually is much larger than mathematics; in fact, it extends to all of systematic inquiry.