MathScheme

MathScheme is a project to develop a new approach to mechanized mathematics in which computer algebra and computer theorem proving are merged without sacrificing power or soundness. The first goal of the project is to develop a formal framework that integrates and generalizes symbolic computation and formal deduction. The second project goal is to design and implement a mechanized mathematics system based on the formal framework. The long-range goal is to build, on top of the mechanized mathematics system, an interactive mathematics laboratory that provides an integrated set of tools for facilitating and managing mathematical reasoning.