×

Formalized mathematical content in lecture notes on modelling and analysis. (English) Zbl 1418.97001

Rabe, Florian (ed.) et al., Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11006, 125-130 (2018).
Summary: 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.
For the entire collection see [Zbl 1392.68030].

MSC:

97U99 Educational material and media and educational technology in mathematics education
68U15 Computing methodologies for text processing; mathematical typography
97I10 Comprehensive works on analysis education

Software:

LaTeX
PDFBibTeX XMLCite
Full Text: DOI