At present there are large computer programs capable of representing mathematical proofs (such as NuPrl) and large computer programs capable of symbolic computation (such as Macsyma), and many theorem-proving programs that try to find proofs. But these three capabilities are nowhere present in the same system. In this project, a single system smoothly integrating symbolic computation and representation of mathematical proofs will be built, and supplemented with proof-finding algorithms. A prototype version has already been able to generate automatically an epsilon-delta proof of the continuity of f(x) = x^3. The system to be built will be able to generate many other epsilon-delta proofs and other more complicated proofs in analysis. ***
