MathScheme: Project Description

The mission of mechanized mathematics is to develop software systems that support the process people use to create, explore, connect, and apply mathematics. Working mathematicians routinely leverage a powerful synergy between deduction and computation. The artificial division between (axiomatic) theorem proving systems and (algorithmic) computer algebra systems has broken this synergy. To significantly advance mechanized mathematics, this synergy needs to be recaptured within a single framework. MathScheme [6] is a long-term project being pursued at McMaster University with the aim of producing such a framework in which formal deduction and symbolic computation are tightly integrated. In the short-term, we are developing tools and techniques to support this approach, with the long-term objective to produce a new system.