Sound mathematics is essential in all modern technological developments. As we build increasingly complex systems, mathematical reasoning becomes more difficult and error-prone. This is particularly true for software systems. A mechanized mathematics system (MMS) is required that can support, improve, and – where possible – automate mathematical reasoning.

There are presently two major types of MMSs, computer algebra systems and computer theorem proving systems. Computer algebra systems provide algorithms for symbolic computation. They are relatively fast and easy to use, but they are not rigorously based, untrustworthy, and narrow in scope. Computer theorem proving systems provide tools for creating formal proofs. They are based on well-defined logical foundations, can support a wide range of mathematics, but are difficult to use and often lack the specific knowledge needed to perform many routine computations.

While mechanized mathematics has the potential to revolutionize the design, implementation, and analysis of software systems, contemporary MMSs fall well short of this potential. There are no MMSs today that provide highly integrated symbolic computation and formal deduction capabilities. There have been earlier attempts to add the capabilities of one type of MMS to an existing system of the other type or to combine two existing systems of different type, but these attempts have not been very successful. One cannot add fundamental capabilities as an afterthought.

Our objective is to develop a new approach to mechanized mathematics that combines the strengths of symbolic algebra systems with those of formal deduction systems to yield a system that is both powerful and sound. The first goal of the project is to develop a formal framework that integrates symbolic computation and formal deduction. The framework should allow mathematical knowledge to be represented both declaratively using axioms and procedurally using algorithms, and it should provide a style of mathematical reasoning in which computation and deduction are intertwined.

The second project goal is to design and implement an MMS based on the formal framework. It should provide services for building formal languages, theories, computations, deductions, and mappings between theories – the services that are necessary for mechanizing the mathematics process.

Our long-range goal is to build, on top of the MMS, an interactive mathematics laboratory (IML) that provides an integrated set of tools for facilitating and managing mathematical reasoning. The IML is intended to have the capabilities of both contemporary computer algebra systems and computer theorem proving systems and the means to formalize a wide range of mathematical knowledge.