The Use of Formal Reasoning Technology in Mathematics Education:
Opportunities and Challenges

William M. Farmer

2007

Abstract

Mathematics education is a highly attractive market for applications
of formal languages and reasoning tools.  The number of people who
study mathematics in school and university is enormous, and there is
strong support for improving mathematics education with the aid of
computer technology.  There are also excellent opportunities to use
formal reasoning technology to enhance, if not transform, how students
learn mathematics.  For example, proof assistants offer a way to
reinvigorate the teaching of proof and deductive reasoning in high
school and university.  Great as these opportunities may be, they are
not easy to pursue.  Many challenges stand in their way.  Not the
least of which is the wide-spread scepticism with which formal
reasoning technology is regarded in the mathematics community.  This
talk will discuss these opportunities and challenges and will argue
that bold applications, like an interactive mathematics laboratory
based on formal reasoning technology, have the best chance of
realizing the opportunities and overcoming the challenges.