The Mathematics Understander (MU)

Furse's solution to the problem of testing his theory of learning and memory was to build the CMS model as a computer program, and to use it within a large computer system to learn university level mathematics from special texts. This model is provocatively known as "The Mathematics Understander" (MU), surely a red rag to Roger Penrose, who argues that machines can NEVER understand mathematics. The texts were hand written in a very expressive but formal notation, known as the Formal Expression Language (FEL), and attempted to be faithful to the author's original mathematics textbook. Some preliminary research shows that students find it easier to read FEL texts than the original texts. But, more interestingly MU can learn from these texts too.

The Mathematics Understander (MU) learns pure mathematics by the reading of a text written in FEL. The level of concentration of the agent can be modelled by altering parameters of the CMS, such as the number of features to use when encoding a result. Even the level of "scattiness" of the student can be modelled by adjusting the ratio of old features known already to the system to brand new features created on the fly. Thus the person who is slow to pick up new knowledge can be modelled by using many old features, and few new features.

MU learns the definitions of mathematical concepts as it encounters them, for example the notion of a prime number, like 5, 7, 11, 13 is expressed by an author of a mathematics text as:

Definition
x is prime
if and only if for all n if n divides x then x = 1 or x = n

and would be expressed in FEL as:

Definition 1.3 of prime
x is prime
iff forall n (n divides x => (x = 1 or x = n))

where one assumes that MU has already learned the concept of "divides". Notions such as "iff", "=>", "=" and "or" can also be learned, but so far MU has to have "forall" built into its processing.

When MU reads a theorem, it just remembers it together with various specialisations (operationalizations) that it generates, so that it can be subsequently used in understanding other theorems. If the theorem is followed by a proof, then the proof is checked line by line, and MU gives an explanation of each step in terms of its existing knowledge of mathematics. MU can also solve simple problems, but in general its proof checking is better than its problem solving.

MU has successfully read texts in branches of pure mathematics known as "Classical Analysis", "Group Theory" and "the Calculus", and will shortly be made available over the Internet for downloading for other research groups to use. Furse has published papers in international conferences (including the prestigious IJCAI, and a video) describing his work, and more recently has submitted a lengthy account to the journal "Cognitive Science".

Top Level
Previous Section
Next Section