[Thedu] THedu "green paper" for CAME

[Walther Neuper <wneuper@ist.tugraz.at>]

Dear colleagues in the THedu board,

discussions with Serge, Pedro and others at CICM suggested to spread the 
attached "green paper" in order to include as many people as interested 
in this discussion.

The origin of the attached text is an annual meeting of leading 
mathematics educators ("Mathematik Didaktiker" in German), called CAME 
[1], which was held in conjunction with CADGME in Novi Sad this year.
In that meeting the future of "Computer Algebra in Mathematics 
Education" was discussed, and extending the topic to "Computer Theorem 
Proving" found immediate interest such that a brief written statement 
(1-2 pages) was requested for further discussion within CAME.

In the attachment there is a draft of mine, any comments, suggestions 
for improvements etc are highly welcome --- the statement seems an 
efficient way to inform opinion leaders in the field of mathematics 
education (who are the referees of future proposals ;-)

Looking forward to a vivid discussion in THedu and beyond !
Walther


[1] http://sites.dmi.rs/events/2012/CADGME2012/came.html

came-general-2-WN.pdf
Description: MS-Word document

\documentclass{article}
\usepackage{a4}
\usepackage{times}
\usepackage{latexsym}
%%%

\begin{document}
Draft for a Green Paper

\medskip\textbf{\Large Theorem-Proving Technologies in STEM Education}

\medskip Walther Neuper $\;$ {\tt wneuper@ist.tugraz.at}

\bigskip In comparison to the White Paper ``Theorem-Proving
Technologies in Dynamic Geometry'', this Green Paper goes a step back
from concrete plans on learning scenarios in the practice of
mathematics education, on development of TP-based software supporting
such practice and on educational research accompanying these
practices. Rather, this paper intends to approach the topic with
maximal generality: generality with respect to available Theorem
Proving (TP) technologies as well as generality with respect to all
levels of education in science, technology, engineering and
mathematics (STEM).

So the paper is rather ``green'' than ``white'' in that it tries to
identify topics for fruitful discussions %and possible cooperations
between experts in STEM education and experts in TP technologies
rather trying to propose immediate action.

\paragraph{TP Technologies and Mathematics:} Computer Theorem Proving
(TP) started at the same
time~\footnote{http://en.wikipedia.org/wiki/Automath} as Computer
Algebra (CA), TP and CA combine to Symbolic Computation since that
time, proceeding from numerical computation. Recently and largely
unnoticed in public, applications in science and technology drove the
development of automated (ATP)~\footnote{ATP in geometry is presently
dominated by algebraic methods, i.e. specialised methods which are
efficient, but do not include logics into their representation and
thus do not establish a logical framework as proposed herewith.} and
interactive (ITP) theorem proving technologies, which have become of
major importance for mathematics and computer science in academia and
in industry, in particular in engineering safe-critical systems in
health-care, banking, etc.

Among mathematicians the role of computer TP is not agreed on
generally, Bruno Buchberger's proverb ``mathematics mechanises
thinking'' is still controversial. A common misunderstanding in
respective discussions does not distinguish between the creation/
application of mathematics knowledge and the properties of the formal
knowledge itself: the former is highly creative, the latter is
mechanical, e.g. if can reliably be interpreted by TP. This
misunderstanding should not carry over to mathematics education, in
particular not in questions like the following, which will be varied
and detailed in the sequel:
\begin{itemize}
\item To which extent can (TP-based) software be conceived as a model
of mathematics~?
\item What kinds of learning scenarios are featured by interactive
models of maths~?
\end{itemize}

\paragraph{Systems transparent in their underlying knowledge} come
within reach for designing educational mathematics assistants when
based on TP. For that purpose systems must represent the mathematical
knowledge, they operate on, in a human readable format; TP following
the LCF paradigm
does~\footnote{E.g. http://isabelle.in.tum.de/dist/library/HOL shows Rings,
Fields, Finite\_Set, Divides, GCD, Lim, etc.}.

So, given a proof, a step-wise calculation based on logics (see
``Structured Derivations'' below), or just a formula like $2\cdot\pi$,
a TP system following the LCF paradigm is ready to support tracing
down to the respective types, with related definitions, axioms,
theorems and proofs --- a perfect prerequisite for inquiry-based
learning.

Designing DGS as transparent systems appears particularly promising,
since most of them already incorporate an optional
numerical/analytical representation; so adding a logical
representation of geometric objects just adds another representation.
\begin{itemize}
\item How filter off which details of mechanised knowledge in which learning
situations~?
\item What effects on learning has optional % but permanent
availability of logical representation~?
\end{itemize}

\paragraph{TP can support all phases of problem solving} as, for
instance, identified by PISA's seven {\em foundamental capabilities}:
Except (1) {\em Communication}, TP allows for specific support for
each capability: (2) {\em Mathematising} to formal specifications is a
prerequisite for TP (and might be hidden from learners), (3) {\em
Representation} can easily varied, e.g. in DGS between geometrical to
formal/logical, (4) {\em Reasoning} is the destiny of TP, (5) Devising
{\em strategies} can be experimented with by mechanical support, (6)
{\em Symbolic operations} are exactly represented by TP and finally
(7) {\em Using mathematical tools} might comprise all the other points
within a consistent software framework, not only for maths, but all
STEM.
\begin{itemize}
\item Which TP technologies exactly support which of the above points
(2..6), and how~?
\item Which adaptations are required for which TP technologies to
serve learning~?
\end{itemize}

\paragraph{Software support for step-wise problem solving} comes
withing reach since TP supports all respective capabilities. In
particular, TP automatically checking input avoids exponential
explosion of code for each step: A step-wise solution comprising $7$
steps with $3$ variants each, would require $3^7$ parts of traditional
code, while for TP an input formula just establishes a normal proof
situation (deriving the input from the logical context).

Together with the above mentioned systems' transparency and with
``next step guidance (NSG)'' there is sufficient automation to support
each step like in a good chess program: input is checked, learners
running into problems might backtrack to previous steps, and if got
stuck, NSG proposes how to proceed towards a solution.
\begin{itemize}
\item How to orchestrate TP components in support of step-wise problem
solving~?
\item What would be the value of ``chess-like'' inquiry-based learning
in STEM~?
\end{itemize}

\paragraph{Format of ``self-contained'' mathematical text:} Before the
advent of computers in mathematics education strong traditions have
been established, how a step-wise solution of a problem in STEM should
look like. Hans-Georg Weigand states (thesis no.3 at CAME/ CADGME'12)
that these traditions start to break, since students start to protocol
calls for CAS functions.

On the other hand, ``Structured
Derivations``~\footnote{http://emath.utu.fi/structured.php}
successfully establish a format in high-school mathematics, which is
close to traditional notation {\em and} can be mechanically
interpreted by TP technology, i.e. it is ``self-contained'' for both,
humans and machines.
\begin{itemize}
\item How match requirements of logical rigor with traditions in paper
\& pencil work~?
\item Which level of formal/logical rigor is appropriate at which
level of learning~?
\end{itemize}

\paragraph{Curriculum development based on mechanised math knowledge}
might seem the most futuristic point in this paper. However, in the
course of ongoing development of TP-based mathematics assistants, the
existing knowledge mentioned
above~\footnote{E.g. http://isabelle.in.tum.de/dist/library/HOL shows
Rings, Fields, Finite\_Set, Divides, GCD, Lim, etc.} will grow rapidly
also for education.  The existing {\em deductive} knowledge will be
consistently extended by {\em formal specification} of problems in
STEM, and also with {\em algorithmic knowledge} of how to solve these
problems (in several variants).
\begin{itemize}
\item What effort is estimated for covering high-school math by
mechanised knowledge~?
\item Use of mechanised knowledge for planning/evaluating/interfacing
curricula~?
\end{itemize}

\bigskip
\textbf{The above list of topics and questions is not considered exhaustive at all, rather, it intends to initiate discussion between educators and TP experts in order to establish mutual understanding and to direct technology-driven developments towards appropriate services for human education.}

%\paragraph{Strengthen continuity between high-school and university}
\end{document}