Formalized Mathematical Content in Lecture Notes on Modelling and Analysis

摘要

We introduce an approach to include formalized mathematics in regular undergraduate mathematics courses. In order to enable automatic parsing and checking, the LATEX. code of our lecture notes systematically uses strict syntax conventions for all definitions and theorems, including in particular an unambiguous grammar for all formulas. Resulting from several years of experience, we present a body of about 1000 pages of notes for a course on modelling and a sequence of three courses on analysis and calculus which are a regular part in the undergraduate mathematics curriculum at the University of Constance. We explain the basic structure of the formalization and its syntax and discuss the practicability of the approach.