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 and gave us the first general definition of functions. 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.). However, Russell discovered a paradox in Frege's work and proposed type theory as a remedy. Type theory later on played an influential role in the semantics of natural and programming languages. But, unfortunately, the direction taken by Frege and Russell did not appeal to the mathematicians.

- Logical languages do not have linguistic categories.
- Logical languages are not a satisfactory communication medium.
- Worst of all, a logician's formalization of a mathematical text loses the original structure and is thus of little use to ordinary mathematicians.

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:

- The Choice of the underlying logic (first/second order?, constructive/classical?, etc.)
- The Choice of how to implement concepts (equational reasoning, induction, etc.).
- The Choice of the proof checker: Coq, Isabelle, PVS, Mizar, etc.

- An informal mathematical proof will cause headaches as it is hard to turn in one big step into a (series of) syntactic proof expressions.
- During the checking of mathematics, the informal proof is replaced by a complete proof where every detail is spelled out. Very long expressions replace the clear mathematical text and this is useless to ordinary mathematicians.

In this tutorial, I argue that both the logic for mathematics and the computation of mathematics have forgotten the language of the mathematician and especially the natural language part. I then provide a language simply based on functions which I show to be the underlying part of the mathematician's vernacular and show how the original mathematical text is an interleaved version of this function part together with the natural language part. The main observation is that so far, during the formalisation and implementation of the natural language texts of mathematics, huge jumps have been made which left the mathematicians behind and which ignored natural language. I argue that it is important for the linguist, mathematician, computer scientist and logician to co-operate in order to formalise and computerise the original natural language texts of mathematics.

Although we only consider texts from mathematics, the method described here can also be applied to other domain specific texts written in natural language.

It is expected that participants in the seminar will have a basic understanding of set theory, functions and statements of predicate logic. Luisa Marti has given a good list of exercises to prepare readers in this area.