Research Project
Pythagoras: Machine support for semi-formalised proof oriented mathematics
Zhaohui Luo
Dept of Computer Science
Royal Holloway, University of London
Funded by EPSRC, grant ref. GR/R84092 (Apr. 2003 - Dec 2006)
In collaboration with Prof. Peter Aczel from University of Manchester
Abstract of the project proposal
Machine support for both numerical and symbolic computational mathematics has been very
successfully used in mathematics, science and education. This proposal aims to investigate the issues
involved in the achievement of such support for proof oriented mathematics. We believe that the theory
and technology of interactive theorem proving can be effectively applied to building tools to help research
mathematicians as well as students of mathematics in their proof development effort. We believe that a
key to this is to focus not on the full formalisation of mathematics but on what we here call
semi-formalised mathematics. This is mathematics which is completely formal as far as the formulation
of definitions and results is concerned, but where proofs are allowed to have steps which may not be
instances of rules of inference, but instead are documented with various kinds of less formal evidence for
the step. We shall study the theory and techniques needed to build supporting computer environments for
the development and presentation of semi-formal mathematics. Our method is to implement a generic
environment based on an existing proof development system. We will develop and implement techniques
of meta-variables in multiple-contexts that will provide effective support for the representation and
development of semi-formal proofs. The evaluation will be conducted via case studies for educational
uses of our tools in Mathematics and Computer Science courses.
Back to Zhaohui Luo's
home page.