EJMT Abstract

Presently Computer Algebra Systems, Dynamic Geometry Systems and Spreadsheets cover most of e-learning in high-school mathematics and as well are used for education in formal parts of science. Recently and largely unnoticed in public, the academic discipline of interactive and automated Theorem Proving (TP) has become of major importance for mathematics and computer science.

This paper considers the promises of TP technology for education in science, technology, engineering and mathematics at the full range of levels from high-school to university.

Starting from prototypes of TP-based educational mathematics systems, conceptual foundations are considered: TP-based software which implements reasoning as an essential part of mathematical thinking technology. Educational objectives for the development of TP-based systems are discussed and concluded with some predictions on possible impact of TP-based educational mathematics assistants.

The final conclusion suggests to announce the emergence of a new, TP-based generation of educational mathematics software.