“An Integrated Framework For Computer Algebra
And Computer Theorem Proving”

Welcome to Our Website!

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.

Research Media has published a 3 page article which gives a longer overview of our high level goals.