Learning University Mathematics

Abstract

Doing Mathematics at University level is a complex task that needs to use large amounts of knowledge learned through experience. The program MU, Mathematics Understander, reads mathematics texts expressed in the Formal Expression Language (FEL), and provides explanations of the proof steps and solves simple problems. MU has successfully checked proofs in group theory and classical analysis, and solved simple problems in group theory. To achieve this performance MU needs to use a large quantity of mathematical knowledge, all of which is learned from the reading of texts, it being impractical to hand program such knowledge. A combinatorial explosion is avoided by use of the Contextual Memory System (CMS) which ensures that important results are easy to access, and unimportant results more difficult. It is further argued that for a machine to be able to check complex proofs it is necessary that its knowledge is organised in a form so that the relative importance of results is used for ret...