Facilitating the start into high level math studies

One observation which was fundamental for the $\mmath$-project can, in fact, be made every fall among the new math students: Very quickly, they seem to be frustrated and overhelmed by the amount of new content and the new demands. In particular, the weekly exercises appear incomprehensible or even impossible to solve. As a result, many students quit their course of studies already around Christmas. Among the remaining, a failure rate of 50 to 60 percent in the exams at the end of the first semester is not uncommon and even students who had very good math grades in secondary school are troubled by this trend.

This raises the question about the difference between math at school and university level. What skills are demanded at university, but neglected at school? Trying to answer these questions was one of the starting points for the $\mmath$-project.

By supervising and accompanying many beginner courses, it began to show that the formal aspects of mathematics are causing much of the trouble among the students.

Traditionally, math lectures are content driven which means that the presentation of concepts (like sequences or metric spaces) and results about them (like convergence theorems) play the dominant role. In comparison, technical aspects which group around the careful and intentional use of precise syntax and deduction rules are addressed implicitly on a learning-by-doing basis. Without dedicated lectures on this topic, students have to discover the importance of the underlying formal structure largely on their own by observing experienced mathematicians using it and by getting a weekly feedback in the tutorials. Unfortunately, many students fail at this task.

In order to offer support, our idea was to carve out all these rules and write them down explicitly in some sort of instruction manual which describes the structure precisely while being close to the mathematical reality of first year students. This led to the development of a formal language whose syntax parallels normal mathematical style and whose semantics describes the rules of logical arguing in a way which is suitable even for preliminary courses.

In addition, the idea came up to develop a proof checking program which verifies a text written in this language with respect to the stated rules. This program should serve as a proof that the stated rules are formulated precisely and unambiguously (otherwise they would not be checkable by a computer). Moreover, as the program figuratively mimics parts of the mathematical working process, it could help students to adopt this new way of thinking.

Some aspects of this formal language were used to redesign basic calculus and modeling courses with a stronger emphasize on formal aspects. The result is a number of lectures notes.