Symbolic Computation Group

Mechanized mathematics is the use of computers to automate, manage, and improve mathematical practice. Started in 2001 at McMaster University, MathScheme is a project to develop a new approach to mechanized mathematics in which computer theorem proving and computer algebra are integrated and generalized. Three ideas are central to the approach. (1) Context is represented by biform theories which can include both formulas and algorithms as axioms. (2) Mathematical knowledge and reasoning is distributed across a network of interconnected biform theories. (3) Formal deduction and symbolic computation are merged into a single activity called derivation. The approach is strongly influenced by the IMPS theorem proving system and the Axiom computer algebra system. This talk will give an overview of MathScheme's goals, accomplishments, and challenges.

This is joint work with Jacques Carette and Martin v. Mohrenschildt.