Abstract: MathLang: A framework for computerising Mathematics.

Fairouz Kamareddine

We report on the findings of the MathLang project which started in 2001 by Fairouz Kamareddine and Joe Wells and which includes Manuel Maarek and Krzyztof Retel

Frege was frustrated by the use of natural language to describe mathematics. In the preface to his Begriffsschrift he says:

"I found the inadequacy of language to be an obstacle; no matter how unwieldy the expressions I was ready to accept, I was less and less able, as the relations became more and more complex, to attain the precision that my purpose required."

Frege therefore presented in his Begriffsschrift, the first extensive formalisation of logic giving logical concepts via symbols rather than natural language. Frege developed things further in his Grundlagen and Grundgesetze der Arithmetik which could handle elementary arithmetic, set theory, logic, and quantification. In his Grundlagen der Arithmetik, Frege argued that mathematics can be seen as a branch of logic. In his Grundgesetze der Arithmetik, he described the elementary parts of arithmetic within an extension of the logical framework of Begriffsschrift. Frege's tradition was followed by many others: (Russell, Whitehead, Ackermann, Hilbert, etc.). Russell discovered a paradox in Frege's work and proposed type theory as a remedy. Advances were also made in set theory, category theory, etc., each being advocated as a better foundation for mathematics. But, none of the logics proposed satisfies all the needs of mathematicians. In particular, they do not have linguistic categories and are not a satisfactory communication medium. Moreover:

In the second half of the twentieth century, programming languages were being developed and this led to the creation of softwares, systems and tools to computerize and check mathematics on the computer, and to give some help and assistance to teachers, students, and users of mathematics. But, a mathematical text is structured differently from a machine-checked text proving the same facts. Making the latter involves extensive knowledge and many choices: Furthermore, checking mathematics on the computer has other problems: This talk argues that both the logic for mathematics and the computation of mathematics have forgotten the mathematician and the language of mathematics during their development. I start from de Bruijn's mathematical vernacular which he refined almost twenty years after the begin of his Automath project (Automating Mathematics). I compare this vernacular to modern approaches for putting mathematics on the computer (e.g., OMDOC, MathML, versions of XML, etc.) and discuss how we can find a language of mathematics that is open to future developments through logic and computation.