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.