Systematic Theory Exploration:
The Lazy Thinking Paradigm

Bruno.Buchberger@RISC.Uni-Linz.ac.at

Talk at Workshop on Computer Algebra, RIMS, Kyoto University, Japan
March 5, 2003
and
at Computer Science Institute, Kyushi University, Japan
March 7, 2003

Copyright Bruno Buchberger 2003.

Copyright Note:  This file may be copied and stored under the following conditions:

         - the file is kept unchanged and includes the copyright note
         - a message is sent to buchberger@risc.uni-linz.ac.at
         - if the material is used then this talk should be cited appropriately.

Overview

Goal

Systematic Theory Exploration

The talk is on "systematic theory exploration":

How can we systematically invent and prove,

theorems and

algorithms

in  the frame of a given theory (= knowledge on given concepts)?

Proving and Programming

Proving and programming is basically the same intellectual activity.

Application of theorems and execution of algorithms (computation) is basically the same.

What Does "Systematically" Mean?

"Systematically":

if you follow the rules, only a little thinking is necessary,

automation or, at least, semi-automation is possible.

Of course, the thinking goes into the rules!

Possible Automation

The strategy is independent of math systems  or a particular math system.

However, in the Theorema system, many of the steps described in this talk can already be executed automatically.

Formal Theory Exploration

"Theory Exploration" Paradigm as an Alternative to "Isolated Theorem Proving" Paradigm

B. B.
Theory Exploration Versus Theorem Proving
Proceedings of the Calculemus' 99 Workshop, Electronic Notes in Theoretical Computer Science, 23/3, Elsevier, 1999.

B. B. 
Theory Exploration with Theorema. 
In: Proceedings of SYNASC 2000 (2nd International Workshop on Symbolic and Numeric Algorithms in Scientific Computing), Oct.4-6,2000, Timisoara, Rumania, (T.Jebelean,V.Negru,A.Popovici eds.), Analele Universitatii Din Timisoara, Ser.Matematica-Informatica, Vol.XXXVIII, Fasc.2, 2000, pp.9-32.

Isolated Theorem Proving

knowledge base      (Overscript[     ⊨
      theory,        ?])       goal formula

Prove[goal,  
      using -> knowledge–base,  in -> theory,  
      by -> proof–method]

Theory Exploration

Given a knowledge base (in a certain theory) invent and prove "all" possible goal formulae such that

knowledge base      (Overscript[     ⊨
    
      theory ,        ])       goal formula

More specifically,

given a "complete knowledge base" on certain given notions,

invent and prove a "complete" system of elementary formulae that describe the interplay of (one or several) new notions with the given notions "completely".

"Complete" knowledge: All other knowledge can be derived by "easy" reasoning (e.g. "rewriting", "symbolic computation").

Theory Exploration in More Detail: Exploration Situations

An "exploration situation" is characterized by the following parameters:

a collection C of known concepts

a collection K of facts that (are thought  to) "completely" describe the interactions (interrelations) among the known concepts

a new concept N

axioms (e.g. definitions) A  that relate the new concept with the known concepts

???  a collection G of goal propositions that (are thought to) "completely" explore the interaction between the new concept and the known concepts.

Theory Exploration in More Detail: How Does One Find "Complete" Knowledge for the New Notion?

Bottom-up: Explore "all" possible interactions of the new notion(s) with the given notions and start with the "simple" ones. (See [B.  2000, Timisoara Proceedings].)

Top-down: Explore by the "lazy thinking paradigm". This is the topic of this talk.

The Lazy Thinking Paradigm

Lazy Thinking: Attempt a Proof, Analyze the Failure,  and Conjecture a Lemma.

We start from an exploration situation (C, K, N, A, G) with an "interesting" goal G.

We attempt to find a proof of G (using an "appropriate" proof method P).

If P yields a proof:  ☺.  (Add G to the knowledge base!)

If P fails:
-  analyze the failing proof situation (current knowledge base and current goal) and
-  conjecture a lemma L that would make the proof possible.

Apply the principle recursively using L as the new goal.

Application of this principle, in the positive case,

does not only yield a proof of the initial goal G

but also fills up the knowledge base for the new concept N.

The Role of Automation

The Lazy Thinking Paradigm is independent of

whether or not the available prover P is automated

whether or not the invention of "interesting" initial goals G is automated

whether or not the analysis of failing proofs is automated

whether or not invention of "useful" intermediate lemmata is automated.

However, increasing automation is possible in all four areas above and is a central goal of the Theorema project.

The principle is, however, only applicable if the (automated) prover P

produces proofs in "natural style"

and produces a proof object also in the case of failure.

References on Theorema

www.theorema.org

B. B., C.Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W.Windsteiger.
The Theorema Project: A Progress Report.
In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000 Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, August 6-7, 2000, St.Andrews, Scotland, M.Kerber and M.Kohlhase eds.), A.K.Peters, Natick, Massachusetts, pp.98-113.

Also see the talk by K. Nakagawa.

Automation of Inventing "Interesting" Goals

Interesting goals often come from "real life".  Example: "I want to sort".

Interesting goals often come from mathematical "experience": In my view, mathematical experience can be cast in

problem types (example: equations)

knowledge types (example: rings)

method / algorithm types (example: divide-and-conquer).

The choice of interesting goals, in the future, may be automated by trying goals from libraries of  problem / knowledge / method types.

Automation of Failure Analysis and Conjecture Generation

We will see examples.

Case Study: Commutativity of Addition

Exploration Situation

Here and in the subsequent examples we use the Theorema syntax, see [B.B et al., 1997, 2000].

Known concepts: '0' (zero), \(TraditionalForm\`\(\('\) \(□\^+\)\)\)' (successor function).

Knowledge about known concepts: induction axiom(s)

\(∀ \+A\((\((A[
                0] ∧ ∀ \+x\((A[x]⟹
                    A[\(x\^+\)])\))\)⟹\(∀ \+x A[
              x]\))\)\)

New concept: '+' (addition).

Axioms (definition) that relate the new concept with the known concepts:

Definition["addition",any[m, n],
	({{m + 0 = m, " +0:"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + .:"}})]

Goal propositions: all formulae of the form

(Underscript[∀ , (Subscript[x, 1]), …, (Subscript[x, n])])L = R

where L and R are terms in '0', '\(TraditionalForm\`\(□\^+\)\)',  '+', and the variables ' (Subscript[x, 1])', …, ' (Subscript[x, n])'.

An Appropriate Proving Method

An appropriate proving method, an induction method that recurs over the variables, is implemented in Theorema, see the examples.

Examples of Proofs

A Very Simple Theorem

For proving the following proposition

Proposition[\("zero from left", any[n], 
	
      0 + n = n\)]

we execute the following Theorema call:

Prove[Proposition["zero from left"],
	using -> Definition["addition"],
                  by -> NNEqIndProver]

Other Theorems that Can be Proved by this Method

Similarly, proofs for the following propositions can be generated automatically by the above method.

Proposition[\("addition from left", 
      any[m, n], 
	\(m\^+\) + n = \(\((m + n)\)\^+\)\)]

Prove[Proposition["addition from left"],using -> Definition["addition"],by -> NNEqIndProver]

Proposition[\("associativity of addition", 
      any[m, n, p], 
	\((m + n)\) + p = m + \((n + p)\)\)]

Prove[Proposition["associativity of addition"],using -> Definition["addition"],by -> NNEqIndProver]

A Failing Proof

The following proposition cannot yet be proved by this (very simple) proof method.

Proposition["commutativity of addition",any[m, n],
	({{m + n = n + m, " + = "}})]

Failing proof:

\(\(Prove[Proposition["commutativity of addition"], 
	
        using -> ⟨Definition["addition"]⟩, 
	by -> NNEqIndProver, 
	
        ProverOptions -> {TermOrder -> LeftToRight}, 
        transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> {Proved, 
                Failed}}];\)\)

The prove method could be made more powerful.
Is not the issue in this talk!

Rather: A strategy,  how fixed prove methods can be applied in the context of exploring entire theories instead of proving isolated theorems.

By good a good strategy for theory exploration, weak prove methods may become strong!

In other words, by a good exploration strategy, weak researchers (professors, students, ...) may become strong.

Exploration by Lazy Thinking

Automated Lazy Thinking

Successful proof and  invention of additional knowledge by the "cascade", i.e. "lazy thinking" consisting of

a prover

a conjecture generator (= failure analyzer + conjecture extractor).

In Theorema,

the above induction prover,

a conjecture generator (= failure analyzer + conjecture extractor) for the induction prover

and the "lazy thinking" exploration cycle

are implemented. Thus, you press a button and the "theory of commutativity is explored automatically".

\(\(Prove[Proposition["commutativity of addition"], 
	
        using -> Definition["addition"], 
        by -> Cascade[NNEqIndProver, ConjectureGenerator], 
        ProverOptions -> {TermOrder -> LeftToRight}];\)\)

Some Observations

Automated failure analysis and conjecture extraction was easy in the case of this theory.

Lazy thinking:

easy thinking

does not only prove but invents.

Where did first conjecture (commutativity) come from?

"experience"  (a knowledge type from a library of knowledge types: "abelian semi-group etc."), see next case study,

systematic set-up of "first interactions"  (suggests the left-hand side of commutativity but cannot guess the right-hand side!)

Case Study: Sorting

Preliminary Remark

In this case study, the emphasis is on the application of the lazy thinking paradigm and not on automation.

Some / most of the proofs can be generated automatically in the current version of Theorema.

Also, automated proof analysis and conjecture extraction used in this case study seem to be easy enough for automation in Theorema. Not yet done.

The Problem of Sorting

The Unknown Sorting Function

sorted[X]  ... "a sorted version of X",  "sort X",

'S' ... a unary function constant,

'X' ... a variable ranging over objects.

Problem Specification (The Correctness Theorem)

The statement of the desire / problem can also be viewed as the "correctness theorem" for the (unknown) process 'sorted'.

Theorem[\("sorted yields sorted version", 
\(∀ \+X\)\+\(is–tuple[X]\)is–sorted–version[X, 
          sorted[X]]\)]

is–tuple[X] ... "X is a tuple",

'is–tuple' ... a unary predicate constant (describing a "type").

Complete Knowledge about the Problem

For solving the problem, it must be "completely understood".

I.e., we should have a "complete knowledge base" on the predicate 'is–sorted–version'.

See other file.

The Proof Call

Let's now try to prove the correctness theorem under the assumption that we have knowledge (a "theory") on 'is–sorted–version':

\(Prove[
      Theorem["correctness for sorting by merging"], 
using -> 
        Theory["is sorted version"], 
by -> \(\(...\)\(...\)\) .. ]\)

Lazy Thinking Round 1: Use Problem Definition

We Prove Until We are Stuck

By a few natural predicate logic proof steps, using knowledge from the Theory["is sorted version"], the following proof attempt is easily generated (i.e. it can be generated automatically by the Theorema system):

We try to prove, for arbitryX,

is–sorted–version[X, sorted[X]]

assuming

is–tuple[X]

In fact,

is–sorted–version[X, sorted[X]]

⇔  (by Definition["is sorted \
version"])

∧{({{is–tuple[sorted[X]]}, {is–permuted–version[X, sorted[X]]}, {is–sorted[sorted[X]]}})}

Hence, it suffices to prove the above

is–tuple[
      sorted[X]], 
is–permuted–version[X, 
      sorted[X]]

and

is–sorted[sorted[X]].

Here we are stuck (because we don't have any knowledge on 'sorted' so far).

We analyze the Failure and Conjecture Lemmata

>From the proof attempt we can learn that, in fact, the following three lemmata are sufficient for completing the proof. ("Collect" all temporaray assumptions and "generalize" the "arbitrary but fixed" constants into universally bound variables!)

Lemma["sorted yields a tuple", 
      any[is–tuple[X]], 
is–tuple[sorted[X]]]

Lemma["sorted yields a permuted version", 
      any[is–tuple[
          X]], 
is–permuted–version[X, 
        sorted[X]]]

Lemma["sorted yields a sorted object", 
      any[is–tuple[X]], 
is–sorted[sorted[X]]]

The Trivial Cases

>From pressing the proof a step further, we could obtain some suggestions of how 'sorted' should be defined for the trivial tuples.

However, let's immediately move to the next, more interesting, step in the exploration.

Lazy Thinking Round 2: Unfold Algorithm Type

The Principle of Unfolding Algorithm Types

Now we have to be creative and "invent" 'sorted'.

However, instead of inventing 'sorted' "by individual ingenuity", we use the following "unfold algorithm types" strategy:

sketch the algorithm 'sorted' in terms of auxiliary functions using one of the algorithm types from a library of algorithm types,  *)

try to prove the desired theorems using the current sketch,

analyze the failure, yielding problem specifications for the auxiliary functions.

For obtaining more refined versions of the auxiliary functions, apply this structuring principle by algorithm types recursively.

*) Surprisingly, although there are thousands of algorithms, there are only a few "algorithm types"!

'Sorted' by "Divide and Conquer"

Algorithm["sorted",any[is–tuple[X]],
sorted[X]={({{special[X], ⇐, is–special[X]}, {composed[
sorted[
                      left–split[X]], 
sorted[
                      right–split[X]]], ⇐, otherwise}})}  ]

where 'special', 'is–special', 'composed', 'left–split', and 'right–split' are just names. Their meaning (properties and definition in terms of more elementary auxiliary functions) will evolve during the next steps of the exploration process.

'special' and 'is–special'

Trying to prove the above three lemmata will easily lead to the suggestion for 'special' and 'is–special':

Algorithm["sorted",any[is–tuple[X]],
sorted[X]={({{X, ⇐, is–trivial–tupel[X]}, {composed[
sorted[
                      left–split[X]], 
sorted[
                      right–split[X]]], ⇐, otherwise}})}  ]

General Case

We now attempt proofs for the above three lemmata using the additional knowledge provided in the definition Algorithm["sorted"].

Lazy Thinking Round 2.1: Sorted Yields a Tuple

Proof Start: Noetherian Induction

We want to prove:

Lemma["sorted yields a tuple", 
      any[is–tuple[X]], 
is–tuple[sorted[X]]]

We attempt a proof by Noetherian induction on ≻. (This proof technique is suggested by the outermost universal quantifier ranging over tuples!)

For this, we take X arbitrary but fixed and assume

(A)     is–tuple[X]

and

(induction hypothesis)       (Underscript[((Underscript[∀ , is–tuple[Y]])), X ≻ Y])is–tuple[
            sorted[Y]].

We have to prove

is–tuple[sorted[X]].

Case: is–special[X].

In this case,

is–tuple[sorted[X]]

↔ by Algorithm["sorted"]

is–tuple[special[X]]

↔ by (A)

true.

Case: ¬ is–trivial–tuple[
            X].

In this case,

is–tuple[sorted[X]]

← by Algorithm["sorted"]

is–tuple[
        composed[
sorted[s1[X]], 
sorted[
            s2[X]]]].

Here we are stuck. However, analyzing the last proof situation, we see that we could go on - using the induction hypothesis - if we knew the following lemmata.

(Again, these lemmata can be conjectured by the method: "Collect current assumptions and goals and replace ground terms by variables.")

Conjectures for Lemmata for 'left–split', 'right–split', and 'merged'

Lemma["splits are tuples",any[is–tuple[X]],with[¬ is–trivial–tuple[X]],
({{is–tuple[left–split[X]]}, {is–tuple[right–split[X]]}})  ]

Lemma["splits are shorter",any[is–tuple[X]],with[¬ is–trivial–tuple[X]],
({{X ≻ left–split[X]}, {X ≻ right–split[X]}})  ]

Lemma["merged yields tuple", 
      any[is–tuple[X, Y]], 
is–tuple[
        composed[X, Y] ] ]

Lemma["splits are shorter"] is just what we need for the termination of Algorithm["sorted"] anyway.

The above lemmata are "desires" for the auxiliary functions 'lef–split' etc. They will be the starting point for applying the lazy thinking paradigm recursively.

Continuation of Case:   ¬is–trivial–tuple[X].

Having these lemmata we could continue with the proof as follows:

is–tuple[
      merged[
sorted[
          left–split[X]], 
sorted[
          right–split[X]]]]

\(\(\(←\)\(\ \)\(by\ Lemma["merged yields tuple"]\)\), 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \((induction\ hypothesis)\), 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Lemma["splits are tuples"], 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Lemma["splits are shorter"]\)

(A) and case assumption.

Lazy Thinking Round 2.2: Sorted Yields Permuted Version

Proof Start: Noetherian Induction

We want to prove

Lemma["sorted yields a permuted version", 
      any[is–tuple[
          X]], 
is–permuted–version[X, 
        sorted[X]]]

We attempt a proof by Noetherian induction on ≻:

For this, we take X arbitrary but fixed and assume

(A)     is–tuple[X]

and

(induction hypothesis)       (Underscript[((Underscript[∀ , is–tuple[Y]])), X ≻ Y])Y ≈ sorted[
              Y].

We have to prove

X ≈ sorted[X].

Case: is–special[X].

In this case,

X ≈ sorted[X]

↔ by Algorithm["sorted"]

X ≈ special[X].

↔ by Lemma["reflexivity of \
≈"]

↔ true.

Here we are stuck. We could complete this proof if we knew the following lemma:

Lemma["trivial tuples are permuted versions", 
      any[is–trivial–tuple[
          X]], 
X ≈ X ]

This is a property of ≈. Hence, we can assume that this is part of the "complete" knowledge on the known concept ≈. (We mark this as one of the "absolutely necessary" / "minimal" properties of the known concepts.)

Case: ¬is–trivial–tuple[X].

We attempt a proof for the second case:

In this case,

X ≈ sorted[X]

↔ by Algorithm["sorted"]

X ≈ 
      composed[
sorted[
          left–split[X]], 
sorted[
          right–split[X]]]

Here we are again stuck. However, analyzing the last proof situation (by collecting assumptions and goals and generalizing ground terms by variables), we see that we could go on - using the induction hypothesis - if we knew Lemma["splits are tuples"], Lemma["splits are shorter"], and the following lemma:

Lemma["merged yields permuted version", 
      any[is–tuple[X, Y, Z]], 
      with[left–split[X] ≈ Y, 
        right–split[X] ≈ 
          Z], 
X ≈ composed[Y, Z]]

This is a property on the new concepts 'merged', 'left–split', and 'right–split'. Thus, it will be a goal for the next, lower, round of lazy thinking. It cannot be assumed as part of the "absolutely necessary" knowledge on the known concepts!

Continuation of Case:   ¬is–trivial–tuple[X].

Having these lemmata we could continue with the proof as follows:

X ≈ 
      merged[
sorted[
          left–split[X]], 
sorted[
          right–split[X]]]

← by Lemma["merged yields permuted \
version"]

is–tuple[X], 
is–tuple[
      sorted[left–split[X]]], 
is–tuple[
      sorted[right–split[X]]], 
left–split[
        X] ≈ 
      sorted[left–split[X]], 
right–split[
        X] ≈ sorted[right–split[X]]

\(\(\(←\)\(\ \)\(by\ \((induction\ hypothesis)\)\)\), 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Lemma["splits are tuples"], 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Lemma["splits are shorter"]\)
               Lemma["sorted by merging yields \
tuples"]

(A) and case assumption.

Lazy Thinking Round 2.3: Sorted Yields a Sorted Object

Proof Start: Noetherian Induction

We want to prove:

Lemma["sorted yields a sorted object", 
      any[is–tuple[X]], 
is–sorted[sorted[X]]]

We attempt a proof by Noetherian induction on ≻:

For this, we take X arbitrary but fixed and assume

(A)     is–tuple[X]

and

(induction hypothesis)       (Underscript[((Underscript[∀ , is–tuple[Y]])), X ≻ Y])is–sorted[
            sorted[Y]].

We have to prove

is–sorted[sorted[X]].

Case:   is–trivial–tuple[X].

In this case,

is–sorted[sorted[X]]

\(\(\(↔\)\(\ \)\(by\ Algorithm["sorted by merging"]\)\)\)

is–sorted[X].

↔ by Lemma["trivial tuples are \
sorted"]

true[X].

The Lemma['trivial tuples are sorted"] is assumed to be in the knowledge base of the known notions (see appendix). (We mark this property as "necessary".)

Case:   ¬is–trivial–tuple[X].

Situation Where Proof Gets Stuck:

In this case:

is–sorted[sorted[X]]

← by Algorithm["sorted by \
merging"]

is–sorted[
        composed[
sorted[
            left–split[X]], 
sorted[
            right–split[X]]]].

Here we are stuck. However, analyzing the last proof situation (by "collecting assumptions and goals and generalizing ground terms to variables"), we see that we could go on - using the induction hypothesis - if we knew the following lemmata:

Lemmata Conjectured by Failure Analysis:

Lemma["merged yields sorted", 
      any[is–tuple[X, Y]], 
      with[is–sorted[X, Y]], 
is–sorted[
        composed[X, Y] ] ]

Lemma["splits are tuples",any[is–tuple[X]],with[¬ is–trivial–tuple[X]],
({{is–tuple[left–split[X]]}, {is–tuple[right–split[X]]}})  ]

Lemma["splits are shorter",any[is–tuple[X]],with[¬ is–trivial–tuple[X]],
({{X ≻ left–split[X]}, {X ≻ right–split[X]}})  ]

This is a property of the new concept 'composed', which we have to treat in the next, lower, round of lazy thinking. Note, how lazy thinking generates the "natural" conjectures for the auxiliary functions, e.g. 'composed'.

In fact, the property required for 'composed' is the crucial part of the problem specification of the problem of "merging".

Continuation of Case:   ¬is–trivial–tuple[X].

Having these lemmata we could continue with the proof as follows:

is–sorted[
        merged[
sorted[
            left–split[X]], 
sorted[
            right–split[X]]]].

\(\(\(←\)\(\ \)\(by\ Lemma["merged yields sorted"]\)\), 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \((induction\ hypothesis)\), 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Lemma["splits are tuples"], 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Lemma["splits are shorter"]\)

(A) and case assumption.

Summary of the Current Stage

Picture

new notion 'sorted'
with a "desired property"
that should be "materialized" (in terms of auxiliary notions and known notions)
in a "proven" way

lazy thinking produces 
                                                      ⇓    a "materialization" of sorted and
                                                                                 auxiliary desired properties on 'sorted' and
                                                                     the auxiliary notions (like 'merged')

known notions (like 'is–tuple', 'prepend', etc.)
with lots of knowledge

Now go on recursively for (the auxiliary desired properties of 'sorted' and) the auxiliary notions, like 'merged'.

Proving and Computing

After completion of this process, the algorithm 'sorted' is verified, i.e. it is guaranteed to work correctly for all inputs.

In Theorema: Most parts of the entire development cycle (including the proofs) can be automated. (Not everything is already working though.)

In Theorema: The verified algorithm can also be executed!

\(Compute[
      sorted[⟨4, 3, 2, 5, 6, 3, 2, 1, 3, 
          5⟩, 
        using -> ⟨Algorithm["sorted"], \  ... ⟩]]\)

⟨1, 2, 2, 3, 3, 3, 4, 5, 5, 
      6⟩

Functors (Not Pursued in this Talk)

Algorithm["sorted",any[is–tuple[X]],
sorted[X]={({{X, ⇐, is–trivial–tuple[X]}, {merged[
sorted[
                      left–split[X]], 
sorted[
                      right–split[X]]], ⇐, otherwise}})}  ]

Every formula, in particular the above algorithm, can be viewed as a "functor":

Given: 'is–trivial–tuple', 'merged', 'lef–split', 'right–split'.

Produce: 'sorted'.

Functors do not only transport computations but also knowledge!

After successful completion of the algorithm and its verification by the lazy thinking strategy,

we could go through all proofs again and

analyze which knowledge on the known notions is absolutely necessary.

We should then store the above algorithm and its correctness theorem together with its "minimal requirements" as a functor.

Case Study: Merging etc.

Not in this talk.

Conclusions

Lazy thinking and creative thinking:

The lazy thinking paradigm has several ingredients:

proving

problem / knowledge / algorithm types

failure analysis and conjecture generation

analysis of minimal requirements and extraction of "re-usable" knowledge.

Each of the ingredients should be studied for possible automation (computer-support).

Thereby, "doing mathematics" will be possible on higher and higher levels.

Re-usable knowledge should be stored in an as general as possible way (functors)

Mathematical knowledge management

All this is the goal of future "mathematical knowledge management" (compare "MKM 2001" at RISC, "MKM 2003" at U of Bologna, "MKM 2004" at U of Birmingham, etc.)

Mathematical Knowledge Management can also be considered as a kind of "Bourbakism of the 21st Century" which, however, is centered on the notion "computer".

The essence of mathematical creativity:

Mathematics is for people who want to be "lazy".   (On the object level.)

For this, from time to time, one must be extremely hard working and insight-ful (= intelligent). (On the meta-level.)

One needs (high+1) human mathematics for automating high mathematics.