MathScheme: Project Description

Jacques Carette, William M. Farmer, and Russell O'Connor

2011

Abstract

The mission of mechanized mathematics is to develop software systems
that support the process people use to create, explore, connect, and
apply mathematics.  One important element of this process is a
powerful synergy between the use of deduction and the use of
computation.  The 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
captured within a single mechanized mathematics system.  That is,
axiomatic mathematics and algorithmic mathematics need to be
integrated into a single framework.  MathScheme is a long-range
project being pursued at McMaster University whose short-term
objective is to develop a new approach to mechanized mathematics in
which formal deduction and symbolic computation are tightly integrated
and whose long-term objective is to produce a new mechanized system
based on this approach.