Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy - Artificial Intelligence and Symbolic Computation - page 237

Isabelle [20], Lego [17], Mizar [3], Nuprl [11], Omega [4]. We also made an
effort in this area, see the Theorema [9] system.
However, as a matter of fact, these reasoning systems are not yet widely
used by the “working mathematicians” (i.e. those who do math research and/or
math teaching). This is in distinct contrast to the current math (computer al-
gebra/numerics) systems like Mathematica, Maple,etc.which,inthepast
couple of years, have finally found their way into the daily practice of math-
ematicians. In this paper, we want to specify a few features of future systems
for algorithm-supported mathematical theory exploration which, in our view,
are indispensable for making these systems attractive for the daily routine of
working mathematicians. These features are:

- Integration of the Functionality of Current Mathematical Systems : Reasoning

systems must retain the full power of current numerics and computer algebra
systems including the possibility to program one's own algorithms in the
system.

- Attractive Syntax : Reasoning systems must accept and produce mathemat-

ical knowledge in attractive syntax and, in fact, in flexible syntax that can
be defined, within certain limitations, by the user.

- Structured Mathematical Knowledge Bases : Reasoning systems must provide

tools for building up and using (large) mathematical knowledge libraries in
a structured way in uniform context with the algorithm libraries and with
the possibility of changing structures easily.

- Reasoners for Invention and Verification : Reasoning systems must provide

reasoners both for inventing (proposing) and for verifying (proving, disprov-
ing) mathematical knowledge.

- Learning from Failed Reasoning : The results of algorithmic reasoners (in par-

ticular, algorithmic provers) must be post-processable. In particular, also the
results of failing reasoning attempts must be accessible for further (algorith-
mic) analysis because failure is the main source of creativity for mathematical
invention.

- Meta-Programming : The process of (algorithm-supported) mathematical

theory exploration is nonlinear: While exploring mathematical theories us-
ing known algorithmic reasoners we may obtain ideas for new algorithmic
reasoners and we may want to implement them in our system and use them
in the next exploration round. Hence, reasoning systems must allow “meta-
programming”, i.e. the algorithmic reasoners must be programmed basically
in the same logic language in which the formulae are expressed on which the
reasoners work.

I think it is fair to say that, in spite of the big progress made in the past couple
of years, none of the current reasoning systems fulfills all the above requirements.
In fact, some of the requirements are quite challenging and will need a lot more
of both fundamental research and software technology. It is not the goal of
this paper, to compare the various current systems (see the above references)
w.r.t. to these six requirements. Rather, we will first summarize how we tried
to fulfil the first three requirements in our Theorema system (see the web site