Computer-Supported 
Mathematical Theory Exploration

Bruno Buchberger
RISC (Research Institute for Symbolic Computation)
Johannes Kepler University
and
RICAM (Radon Institute for Computational and Applied Mathematics)
Austrian Academy of Science 
Linz, Austria

Invited Talk at
Mathematica Gulf Conference, January 2004
Sultan Qaboos University
Department of Mathematics and Statistics

Copyright Bruno Buchberger 2004.

Copyright Note: This file can be printed, stored and distributed under the following conditions:

- the file is kept unchanged
- this copyright note is included
- a message is sent to Bruno.Buchberger@JKU.at.

If you use the material, please, cite this  talk appropriately.

A Paradigm Shift in Mathematical Software Systems

Goal of This Talk

This workshop: demonstrating the power of current math software systems (like Mathematica).

My talk yesterday: some of the algorithmics (Gröbner bases) behind current math systems.

My talk today: possible future ingredients of math systems.

Current Math Software Systems  = Solving and Simplifying

Solving:

Solve[{x (y^2) - 3  x y + 2 == 
          0, (x^2) y - 5 (x^2) - 2  x y  + 3 == 0}]

How does this work?

F = {x (y^2) - 3  x y + 2, (x^2) y - 5 (x^2) - 2  x y  + 
          3}

Simplifying:

GroebnerBasis[F]

Why Does This Work? The Answer is Beyond Current Math Software Systems.

Theorem[\("B. Buchberger 1965/1970/1979/1983", 
      any[F], 
is–Groebner–Basis[
            F]⟺\(∀ \+\(f, g ∈ F\)remainder[S–polynomial[f, g], F]\) = 0\)]

This theorem also yields an algorithm for computing Groebner bases. (First implementation 1965 on a ZUSE Z23 with 8 K drum memory. Routinely available in all math software systems since ~ 1985.)

Proof of the theorem? Currently beyond the capabilities of math software systems.

Future Math Software Systems: Mathematical Knowledge Management (MKM)

Mathematical Knowledge Management: Should and will support all phases of the process of "doing mathematics":

invent mathematical concepts (notions, operations, functions, predicates, ...), problems, questions, theorems, methods (algorithms)

find known concepts, problems, theorems, methods

prove theorems and the correctness of methods (algorithms)

store concepts, problems, theorems, methods.

1st International Conference on MKM, Sep. 24-26, 2001, at RISC, Austria.
2nd International Conference on MKM, Feb. 16-18, 2003, at U of Bologna, Italy.

Theorema is a First Attempt of an MKM System

Theorema

provides a uniform predicate logic syntax for all of mathematics and tools for structuring large mathematical knowledge bases

aims at computer-supporting proving, solving, and simplifying in one uniform logical and software-technological frame

programmed in Mathematica and heavily using the Mathematica front-end

implements various different new and known methods for computer-supported proving for various areas of mathematics

designed and implemented by Theorema Group directed by B. Buchberger.
 
Senior researchers: Tudor Jebelean, Wolfgang Windsteiger, Temur Kutsia, Markus Rosenkranz.

Former and current PhD students: Elena Tomuta, Franz Kriftner, Daniela Vasaru, Claudio Dupret, Florina Piroi, Koji Nakagawa.

Example: Manipulating Mathematical Text

Initialize Theorema!

Definition[\("limit:", any[f, a], 
	
      limit[f, a]⟺\ \(\(∀ \+ϵ\)\+\(ϵ > 0\)\(∃ \+N\(\(∀ \+n\)\+\(n ≥ N\)\[LeftBracketingBar]f[n] - 
                    a\[RightBracketingBar] < ϵ\)\)\)\)]

Proposition[\("limit of sum", 
      any[f, a, g, 
        b], 
	\((limit[f, a] ∧ 
            limit[g, b])\)\ \ \ \ \  \[Implies] \ \ \ \ \ limit[f + g, 
          a + b]\)]

Definition[\("+:", 
      any[f, g, x], 
	\((f + g)\)[x] = f[x] + g[x]\)]

Lemma[\("|+|", 
      any[x, y, a, 
        b, δ, ϵ], 
	\((\[LeftBracketingBar]\((x + 
                    y)\) - \((a + 
                    b)\)\[RightBracketingBar] < \((δ + ϵ)\))\)\ \ \ \ ⟸\ \ \ \((\[LeftBracketingBar]x - a\[RightBracketingBar] < δ ∧ \[LeftBracketingBar]y - 
                  b\[RightBracketingBar] < ϵ)\)\)]

Lemma[\("max", any[m, M1, M2], 
	
      m ≥ 
          max[M1, M2]\ \ \ \ \  \[Implies] \ \ \ \ \ \((m ≥ 
              M1 ∧ m ≥ M2)\)\)]

Theory["limit",
	({{Definition["limit:"]}, {Definition["+:"]}, {Lemma["|+|"]}, {Lemma["max"]}})]

Example: The PCS Prover

A heuristic proof method (B. Buchberger 2000) for predicate logic.

Generates "natural" proofs.

For formulae with alternating quantifiers.

Prove[Proposition["limit of sum"], 
      using -> Theory["limit"], by -> PCS]

The following proof, including the English explanatory text, is generated completely automatically by our PCS proving algorithm. The proof also contains interesting algorithmic and didactic information!

Example: Set Theory Prover

The Theorema set theory prover, implemented in the PhD thesis of W. Windsteiger, is also based on the PCS principle.

Definition[\("reflexivity", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–reflexive\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x ∈ A\)x ∼ x\)\)\)]

Definition[\("symmetry", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–symmetric\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x, y ∈ A\)\((x ∼ y \[Implies] y ∼ x)\)\)\)\)]

Definition[\("transitivity", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–transitive\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x, y, z ∈ A\)\((x ∼ 
                    y ∧ y ∼ z \[Implies] x ∼ z)\)\)\)\)]

Definition["equivalence",any[∼,A],
is–(Subscript[equivalence, A])[ ∼ ]:⇔∧{({{is–(Subscript[reflexive, A])[ ∼ ]}, {is–(Subscript[symmetric, A])[ ∼ ]}, {is–(Subscript[transitive, A])[ ∼ ]}})} ]

Definition[\("class", 
      any[x, \(\(∼\)\(\(,\)\(A\)\)\)], 
class\_\(A,  ∼ \)[
          x] := {a ∈ A \[VerticalSeparator] 
            a ∼ x ∧ x ∈ A}\)]

Proposition[\("equal classes", 
      any[x ∈ A, y ∈ A, \(\(∼\)\(\(,\)\(A\)\)\)], 
      with[is–equivalence\_A[ ∼ ]], 
x ∼ y \[Implies] \((class\_\(A,  ∼ \)[x] = 
            class\_\(A,  ∼ \)[y])\)\)]

?SetTheoryPCSProver

Prove[Proposition["equal classes"],
\(using -> ⟨Definition["equivalence"], 
            Definition["transitivity"], Definition["symmetry"], 
            Definition["class"]⟩\),
by -> SetTheoryPCSProver,
transformBy -> ProofSimplifier,TransformerOptions -> {branches -> Proved, 
              steps -> Useful},ShowOptions -> {},
\(ProverOptions -> {GRWTarget -> {"goal", "kb"}, AllowIntroduceQuantifiers -> True, 
              UseCyclicRules -> True, DisableProver -> {STC, PND}, 
              ApplyBuiltIns -> {}}\),SearchDepth -> 50]

(Proving needs approximately 2 minutes !! It is generated completely automatically and is in the style of the above proof on limits.)

Exampe: Induction Proofs and the Cascade

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

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

The following call produces a proof attempt. By studying the attempt, one may obtain a conjecture about a useful lemma whose proof would make it possible to complete the proof of commutativity.

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

By the following, completely automatic "cascade", a successful proof of commutativity is generated and, on the way to the successful proof,  additional knowledge (two lemmata) are invented and proved:

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

Below are the five proof notebooks generated automatically by the cascade prover:

Proof Attempt 1 of Commutativity, which Leads to  Conjecturing Lemma 1

Pending proof of (1).

Pending proof of (18).

Proof of the Automatically Conjectured Lemma 1

Proof Attempt 2 of Commutativity, which Leads to Conjecturing Lemma 2

Pending proof of (1).

Proof of the Automatically Conjectured Lemma 2

Successful Proof of Commutativity Using the Proved Lemmata

Example: Proving Booleans of Equalities by Groebner Bases

The Groebner Bases Method for Proving

Groebner Bases method: B. Buchberger 1965, 1970, ...

Formula["Test",any[x, y],
	({{\(\((\ \ \((\(x\^2\) y - 3  x\ )\) ≠ 
                    0)\) ∨ \((\((x\ y + x + y)\) ≠ 
                    0)\) ∨ 
		\((\((\((\(x\^2\) y + 3  x = 
                            0)\) ∨ \((\((\(-2\)\ x\^2 + \(-7\)\ x\ y + 
                                x\^2\ y + 
                                x\^3\ y + \(-2\)\ y\^2 + \(-2\)\ x\ y\^2 + 
                                2\ x\^2\ y\^2)\) = 
                            0)\))\)
	 ∧ \((\((x\^2 + \(-x\)\ y + 
                            x\^2\ y + \(-2\)\ y\^2 + \(-2\)\ x\ y\^2)\) = 
                        0)\))\)\),           "B1"}})]

Prove[Formula["Test"], using -> {}, 
      by -> GroebnerBasesProver]

The following proof is generated completely automatically by the Groebner bases method. Note that the proof also includes an explanation of the method.

Thousands of known (and unknown) geometric theorems and conjectures can be formulated as statements of this form and, hence, can be proved / disproved by the Gröbner bases method.

The two proofs below are examples of proofs generated completely automatically by this method.

Example Pappus' Theorem

Textbook formulation:

Let A, B,  C and A1, B1,  C1 be on two lines and P = A B1 ⋂ A1 B, Q = A C1 ⋂ A1 C, S = B C1 ⋂ B1 C. Then P, Q, and S are collinear.

Input to the system:

Proposition["Pappus",  any[A, B, A1, B1, C, C1, P, Q, S], 
      point[A, B, A1, B1] ∧ pon[C, line[A, B]] ∧ 
          pon[C1, line[A1, B1]] ∧ 
          inter[P, line[A, B1], line[A1, B]] ∧ 
          inter[Q, line[A, C1], line[A1, C]] ∧ 
          inter[S, line[B, C1], line[B1, C]] \[Implies] 
        collinear[P, Q, S]]

Input to the system:

Simplify[Proposition["Pappus"], by -> GraphicSimplifier]

Output generated automatically by the system

End of output

Input to the system:

KnowledgeBase["Pappus_g", 
      any[A, B, A1, B1, C, 
        C1], {{A, {10, 120}}, {B, {100, 150}}, {A1, {25, 
            60}}, {B1,  {120, 50}}, {C, {260, 
            200}}, {C1, {250, 45}}}]

Input to the system:

Simplify[Proposition["Pappus"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Pappus_g"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Pappus"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> True}]

Inserted notebook generated automatically by the system

End of inserted notebook

The Butterfly Theorem

Textbook formulation:

A, B, C and D are four points on circle (O). E is the intersection of AC and BD. Through E draw a line perpendicular to OE, meeting AD at F and BC at G. Show that (OverBar[FE]) = (OverBar[GE]).

Remark:

Using the default coordinate system the algebraic methods are very slow.

Input to the system:

Proposition["Butterfly", any[O, A, B, C, D, EE, F, G], 
      point[O, A] ∧ 
pon[C, 
            circle[O, A]] ∧ 
pon[B, 
            circle[O, A]] ∧ 
pon[D, 
            circle[O, A]] ∧ 
inter[EE, line[A, C], 
            line[B, D]] ∧ inter[F, line[D, A], tline[EE, EE, O]] ∧ 
          inter[G, line[B, C], line[EE, F]]
 \[Implies] 
        distequal[EE, F, G, EE]]

Input to the system:

Simplify[Proposition["Butterfly"], 
      by -> GraphicSimplifier]

Output generated automatically by the system

End of output

Input to the system:

KnowledgeBase["Butterfly_g", 
      any[O, A, B, C, 
        D], {{ O, {100, 100}}, {A, {0, 100}}, {B, {55, 
            190}}, {C, {171, 170}}, {D, {60, 10}}}]

Input to the system:

Simplify[Proposition["Butterfly"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Butterfly_g"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Butterfly"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> False}]

Inserted notebook generated automatically by the system

End of inserted notebook

Example: Inventing and Proving Σ-Terms

Zeilberger, Paule, ... method. Groebner bases for non-commutative polyonomials play a role.

Example: Closed form for the following expression was an open problem for many years! The solution was given in P. Paule,  Computer-Solution of Problem 94-2, SIAM REVIEW Vol.37 (1995), 105-106 using the Paule-Schorn automated conjecture generator / prover.

Formula[\("SIAM series", 
	∑\+\(k = 1, …, n\)\(\(\((\(-1\))\)\^\(k + 1\)\) \((4\ k + 1)\) \(\((2\ k)\)!\)\)\/\(\(2\^k\) \((2\ k - 1)\) \(\((k + 1)\)!\) \(2\^k\) \(k!\)\)\)]

Simplify[Formula["SIAM series"], 
      by -> PauleSchorn–Telescope, 
      built–in -> Built–in["PauleSchorn"]]

Prove[Formula["SIAM series"], 
      by -> PauleSchorn–Telescope, 
      built–in -> Built–in["PauleSchorn"]]

System`FullSimplify[(((((((-1))^(1+k)) (2^(1-2 (1+k))) (2 (1+k))! (2+k))/((1+k)! (2+k)! (-1+2 (1+k))))-(((((-1))^k) (2^(1-2 k)) (2 k)! (1+k))/(k! (1+k)! (-1+2 k))))/((-(((-1))^k) (2^(-2 k)) (2 k)! (1+4 k))/(k! (1+k)! (-1+2 k))))]

Example: Calling External Provers (e.g. Resolution)

Links from Theorema to various existing theorem provers, for example to the Otter prover:

<< "C:\PROGRAM FILES\ATP \
SYSTEMS\TMA2EXTERNAL\THEOREMA2EXTERNAL.M"

Definition["Inclusion",
		({{(Underscript[∀ , A, B])((A ⊆ 
                          B)⟺(Underscript[∀ , x])((x ∈ A)⟹(x ∈ 
                                B))), "⊆:"}})]
	Definition["Union",
		({{(Underscript[∀ , A, x])((x ∈ ⋃A)⟺(Underscript[∃ , Y])((x ∈ 
                                Y) ∧ (Y ∈ A))), "⋃:"}})]
	Definition["Powerset",
		({{(Underscript[∀ , A, x])((x ∈ 𝒫[
                            A])⟺(x ⊆ A)), "P:"}})]

Proposition["Union of powerset includes...",
		({{(Underscript[∀ , A])(A ⊆ ⋃𝒫[
                          A]), "⊆P⋃"}})]

ProveExternal[Proposition["Union of powerset includes..."],using->{Definition["Inclusion"],Definition["Union"],Definition["Powerset"]},by -> Otter]

Proof is generated in an extra notebook. Is a sequence of clauses, not shown here.

Example: Computation Using Functors

A Sparse Polynomials Functor

Definition["pol" ,any[C, T],
pol[C, T] =Functor[P,\(any[c, d, i, m\&_, n\&_, p, q, s, t]\),
	({{𝕤 = ⟨0 ∶ P, 
                        1 ∶ 
                          P, +∶P\[Cross]P -> 
                              P, -∶P -> 
                              P, -∶P\[Cross]P -> 
                              P, *∶P\[Cross]
                                P -> P⟩}, {({{
(Underscript[0, P]) = ⟨⟩}, {(Underscript[1, P]) = ⟨⟨(Underscript[1, C]), 
                                (Underscript[1, T])⟩⟩}, {\(⟨⟩\( + \+P\)q = q\)}, {\(p\( + \+P\)⟨⟩ = p\)}, {\(⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\( + \+P\)⟨⟨d, t⟩, 
                                n\&_⟩ = \[LeftDoubleBracketingBar]⟨c, 
                                    s⟩⌣\((⟨m\&_⟩\( + \+P\)⟨⟨d, t⟩, 
                                        n\&_⟩)\) ⇐ s\( > \+T\)t, 
	⟨d, 
                                    t⟩⌣\((⟨⟨c, s⟩, 
                                        m\&_⟩\( + \+P\)⟨n\&_⟩)\) ⇐ 
                                t\( > \+T\)s, 
	\((⟨c\( + \+C\)d, s⟩)\)⌣\((⟨m\&_⟩\( + \+P\)⟨n\&_⟩)\) ⇐ \((c ≠ \(-\+C 
                                      d\))\), 
\((⟨m\&_⟩\( + \+P\)⟨n\&_⟩)\) ⇐ 
                                otherwise\[RightDoubleBracketingBar]\)}, {\(\(-\+P⟨⟩\) = ⟨⟩\)}, {\(\(-\+P⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\) = ⟨\(-\+C c\), 
                                s⟩⌣\((\(-\+P⟨m\&_⟩\))\)\)}, {\(p\( - \+P\)q = p\( + \+P\)\((\(-\+P q\))\)\)}, {\(⟨⟩\(*\+P\)q = ⟨⟩\)}, {\(p\(*\+P\)⟨⟩ = ⟨⟩\)}, {\(⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\(*\+P\)⟨⟨d, t⟩, 
                                n\&_⟩ = \((⟨⟨c\(*\+C\)d, 
                                      s\(*\+T\)t⟩⟩\( + \+P\)⟨⟨c, 
                                        s⟩⟩\(*\+\(\(P\)\(\ \)\)\)⟨n\&_⟩)\)\( + \+P\)⟨m\&_⟩\(*\+\(\(P\)\(\ \)\)\)⟨⟨d, t⟩, 
                                  n\&_⟩\)}})}})
	]]

Theorema programs are just one special class of formulae!

Generate 3-Variate Polys over the Integers

Theory["F",
	({{Definition["integers"]}, {Definition["power products"]}, {Definition["pol"]}})]

Definition[\("D", 
	ℙ = 
        pol[integers[], power–products[3]]\)]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Theory["F"], Definition["D"]⟩]

\(Compute[\((⟨⟨5, ⟨2, 3, 
                1⟩⟩, ⟨3, ⟨1, 6, 
                3⟩⟩⟩\(*\+ℙ\)\((⟨⟨5, ⟨2, 3, 
                    1⟩⟩, ⟨3, ⟨1, 6, 
                    3⟩⟩⟩\(*\+ℙ\)⟨⟨5, ⟨2, 3, 
                    1⟩⟩, ⟨3, ⟨1, 6, 
                    3⟩⟩⟩)\))\)]\)

⟨⟨125, ⟨6, 9, 
          3⟩⟩, ⟨225, ⟨5, 12, 
          5⟩⟩, ⟨135, ⟨4, 15, 
          7⟩⟩, ⟨27, ⟨3, 18, 
          9⟩⟩⟩

In Mathematica:

(((5  (x1^2) (x2^3) x3 + 3  x1 (x2^6) (x3^3)))^3)

125 (x1^6) (x2^9) (x3^3) + 225 (x1^5) (x2^12) (x3^5) + 
        135 (x1^4) (x2^15) (x3^7) + 27 (x1^3) (x2^18) (x3^9)

Generate 5-Variate Polys over the Finite Field Modulo 13

Theory["F",
	({{Definition["finite field"]}, {Definition["power products"]}, {Definition["pol"]}})]

Definition[\("D", 
	ℙ = 
        pol[finite–field[13], power–products[5]]\)]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Theory["F"], Definition["D"]⟩]

Generate 5-Variate Polys over the 2 Variate Rational Functions over the Finite Field Modulo 13

Theory["F",
	({{Definition["rational"]}, {Definition["power products"]}, {Definition["pol"]}})]

Definition[\("D", 
	ℙ = 
        pol[
quotient–field[
pol[
Galois–field[
                13], 
power–products[
                2]]], 
power–products[5]]\)]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Theory["F"], Definition["D"]⟩]

Example: Automated Algorithm Invention

The Problem of Automated Algorithm Invention (Program Synthesis)

Given:

P .. a problem specification.

Find:

A .. an algorithm that satisfies P (together with a proof of correctness).

Example of a Problem Specification

(Underscript[∀ , is–tuple[X]])is–sorted–version[X,  sorted[X]]

Example of a Knowledge  Base

(Underscript[∀ , is–tuple[X]])(is–sorted–version[X, Y]  ⇔{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})})

({{is–sorted[⟨⟩] }, {(Underscript[∀ , x]) 
                is–sorted[⟨x⟩]}, {\(∀ \+\(x, y, \(z\&-\)\)\)(\(is–sorted[⟨x, y, 
                      z\&_⟩]\)   ⇔{({{x ≥ y}, {\(is–sorted[⟨y, 
                              z\&_⟩]\)}})    })}})

({{⟨⟩≈⟨⟩ }, {\(∀ \+\(y, y\&_\)⟨⟩ ≉ ⟨y, y\&_⟩\)}, {\(\(∀ \+\(x, x\&_, y\&_\)\((⟨x, 
                    x\&_⟩ ≈ ⟨y\&_⟩\  ⇔ \((x ∈ ⟨y\&_⟩ ∧ ⟨x\&_⟩ ≈ 
                      dfo[x, \ ⟨y\&_⟩])\))\)\)\(
\)
          \)}})

({{(Underscript[∀ , x]) 
                x ∉ ⟨⟩}, {\(∀ \+\(x, y, y\&_\)\((x ∈ ⟨y, 
                      y\&_⟩)\)\ \  ⇔ \((\((x = y)\) ∨ 
                    x ∈ ⟨y\&_⟩)\)\)}})

({{(Underscript[∀ , a]) dfo[
                  a,  ⟨⟩] = ⟨⟩}, {\(∀ \+\(a, x, x\&_\)dfo[
                  a, \ ⟨x, x\&_⟩\ ]\) ={({{\(⟨x\&_⟩\), ⇐, x = a}, {\(x⌣
                        dfo[a, \ ⟨x\&_⟩]\), ⇐, otherwise}})} }})

({{\(∀ \+\(y\&_\)\(¬ ⟨⟩ ≻ ⟨y\&_⟩\)\)}, {\(∀ \+\(x, x\&_\)⟨x, 
                  x\&_⟩ ≻ ⟨⟩\)}, {\(∀ \+\(x, x\&_, y, y\&_\)⟨x, 
                    x\&_⟩ ≻ ⟨y, 
                    y\&_⟩\  ⇔ ⟨x\&_⟩ ≻ ⟨y\&_⟩\)}})

\(∀ \+\(x, y\&_\)\((x⌣⟨y\&_⟩ = ⟨x, 
            y\&_⟩)\)\)

\(\(\(∀ \+\(x, y\&_\)\((⟨y\&_⟩⌢x = ⟨y\&_, 
            x⟩)\)\)\(
\)
    \)\)

\(∀ \+X\((is–tuple[
            X]\  ⇔ \ \(∃ \+\(x\&_\)\((X = ⟨x\&_⟩)\)\))\)\)
({{(Underscript[∀ , X])(is–empty–tuple[
                  X]  ⇔ (X = ⟨⟩))}, {(Underscript[∀ , X])(is–singleton–tuple[
                  X]  ⇔ (Underscript[∃ , x])(X = ⟨x⟩))}, {(Underscript[∀ , X])(is–trivial–tuple[
                  X] ⇔ (is–empty–tuple[
                      X] ∨ is–singleton–tuple[X]))}})

({{\(∀ \+\(x, x\&_, y, y\&_\)\((⟨x, 
                    x\&_⟩\  = ⟨y, 
                    y\&_⟩)\) ⇔ \((\((x = 
                      y)\) ∧ \((⟨x\&_⟩ = ⟨y\&_⟩)\))\)\)}, {\(∀ \+\(x, x\&_\)⟨x, 
                x\&_⟩ ≠ ⟨⟩\)}})

(Underscript[∀ , is–trivia–tuple[X]])is–sorted[
        X]

(Underscript[∀ , is–trivial–tuple[X],  is–tuple[Y]])(X ≈ 
            Y ⇔ (X = Y))

({{(Underscript[∀ , is–tuple[X]])X ≈ X}, {(Underscript[∀ , is–tuple[X, Y]])(X ≈ 
                  Y \[Implies] Y ≈ X)}, {(Underscript[∀ , is–tuple[X, Y, Z]])((X ≈ 
                      Y ∧ Y ≈ Z) \[Implies] 
                X ≈ Z)

          }})

({{(Underscript[∀ , is–tuple[X, Y]])(X ≻ 
                  Y \[Implies] (Y ⊁ X))}, {(Underscript[∀ , is–tuple[X, Y, Z]])((X ≻ 
                      Y ∧ Y ≻ Z) \[Implies] 
                X ≻ Z)}})

The "Failing Correctness Proof" Method (B. Buchberger 2001) for Automated Algorithm Invention

The two main ideas:

Use algorithm schemes for guessing possible algorithms.

For each algorithm scheme A, (automatically) attempt a proof that A satisfies P. From the failing proof, derive (automatically) specifications for the subalgorithms.

Find appropriate subalgorithms in an algorithm library or repeat failing correctness proof method for inventing the subalgorithms.

Inventing the Algorithm by Lazy Thinking: First Round

The method first selects an algorithm scheme from a library of algorithm schemes, e.g. the algorithm scheme "divide and conquer":

(Underscript[∀ , is–tuple[X]])(sorted[X]={({{special[X], ⇐, is–trivial–tuple[
                      X]}, {merged[sorted[left–split[X]], 
                      sorted[right–split[X]]], ⇐, otherwise}})})

The following proof attempt is automatically generated in Theorema:

Proof Attempt Begin

For proving the correctness theorem, we use well-founded induction w.r.t. ≻ on X:

We assume

\(is–tuple[⟨xo\&_⟩]\)

and the induction hypothesis

\(\(∀ \+\(is–tuple[Y]\)\)\+\(⟨xo\&_⟩ ≻ Y\)is–sorted–version[Y, 
        sorted[Y]]\)

and we show

\(\(\(is–sorted–version[⟨xo\&_⟩, 
        sorted[⟨xo\&_⟩]]\)\(.\)\)\)

We use the algorithm scheme for 'sorted' and distinguish two cases:

CASE

\(\(\(is–trivial–tuple[⟨xo\&_⟩]\)\(:\)\)\)

In this case, we have to show

\(is–sorted–version[⟨xo\&_⟩, 
      special[⟨xo\&_⟩]]\)

i.e., by the definition of 'is–sorted–version', we have to show

\(\(\(\((G1)\)\ \ \ \ \ \ is–tuple[
        special[⟨xo\&_⟩]]\)\(,\)\)\)

\(\(\(\((G2)\)\ \ \ \ \ \ special[⟨xo\&_⟩] ≈ ⟨xo\&_⟩\)\(,\)\)\)

\(\((G2)\)\ \ \ \ \ \ \(\(is–sorted[
          special[⟨xo\&_⟩]]\)\(.\)\)\)

(G1) is true because of the type requirement for 'special'.

For (G2), by the fact that

(Underscript[∀ , is–trivial–tuple[X],  is–tuple[Y]])(X ≈ 
            Y ⇔ (X = Y)),

it suffices to prove that

\(special[⟨xo\&_⟩] = \(\(⟨xo\&_⟩\)\(.\)\)\)

Here we are stuck.

Proof Attempt End

Requirement Generation

Now we analyze the failing proof situation and conjecture the requirement (can be done completely automatically in Theorema!):

(Underscript[∀ , is–trivia–tuple[X]])(special[X] = 
          X)

We add this requirement to the knowledge base and proceed to the next invention round.

Inventing the Algorithm by Lazy Thinking: Second Round

With this requirement on special we get over the failing proof situation and continue with:

CASE

\(\(\(¬ is–trivial–tuple[⟨xo\&_⟩]\)\(:\)\)\)

In this case, we have to show

\(\(\(is–sorted–version[⟨xo\&_⟩, 
        merged[sorted[
            left–split[⟨xo\&_⟩], 
            sorted[right–split[⟨xo\&_⟩]]]]]\)\(.\)\)\)

For this, by the definition of 'is–sorted–version', it suffices to show

\(\(\(\((H1)\)\ \ \ \ \ \ is–tuple[
        merged[sorted[
            left–split[⟨xo\&_⟩], 
            sorted[right–split[⟨xo\&_⟩]]]]]\)\(,\)\)\)

\(\(\(\((H2)\)\ \ \ \ \ ⟨xo\&_⟩ ≈ 
      merged[sorted[
          left–split[⟨xo\&_⟩], 
          sorted[right–split[⟨xo\&_⟩]]]]\)\(,\)\)\)

\(\((H3)\)\ \ \ \ \ \(\(is–sorted[
          merged[sorted[
              left–split[⟨xo\&_⟩], 
              sorted[right–split[⟨xo\&_⟩]]]]]\)\(.\)\)\)

>From the case assumption, by the type requirements on 'left–split' and 'right–split', the property that 'left–split' and 'right–split' produce shorter tuples, and the induction hypothesis we obtain

\(\(\(is–sorted–version[
      left–split[⟨xo\&_⟩], 
      sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(is–sorted–version[
        right–split[⟨xo\&_⟩], 
        sorted[right–split[⟨xo\&_⟩]]]\)\(.\)\)\)

>From this, by the definition of 'is–sorted–version', we obtain

\(\(\(\((AL1)\)\ \ \ \ \ is–tuple[
        sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AL2)\)\ \ \ \ \ left–split[⟨xo\&_⟩] ≈ 
      sorted[left–split[⟨xo\&_⟩]]\)\(,\)\)\)

\(\(\(\((AL3)\)\ \ \ \ \ is–sorted[
        sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AR1)\)\ \ \ \ \ is–tuple[
        sorted[right–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AR2)\)\ \ \ \ \ right–split[⟨xo\&_⟩] ≈ 
      sorted[right–split[⟨xo\&_⟩]]\)\(,\)\)\)

\(\((AR3)\)\ \ \ \ \ \(\(is–sorted[
          sorted[right–split[⟨xo\&_⟩]]]\)\(.\)\)\)

(H1) follows from (AL1) and (AR1) by the type requirement on 'merged'.

Now we are stuck.

Proof Attempt End

Requirement Generation

It is not so near at hand but, after some thinking, relatively easy to conjecture (and our current Theorema conjecture generating algorithm can do this automatically) that the following requirement on the functions 'left-split', 'right-split' und 'merged'

(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                Z]])), ¬ is–trivial–tuple[X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})

will make it possible to get over the failing proof situation.

We add this requirement to the knowledge base and proceed to the next invention round.

Inventing the Algorithm by Lazy Thinking: Last Round

We now do exactly the same proof attempt once more (or we just jump to the proof situation where the previous proof attempt got stuck.)

This time, the inductive proof will succeed using the added requirement on  'left-split', 'right-split' und 'merged' for proving (H2) and (H3).

What Do We Have Now?

If we now collect the requirements on the functions'special', 'left-split', 'right-split', and 'merged', we see that we invented and proved the following theorem:

If

{({{(Underscript[∀ , is–tuple[X]])(sorted[X]={({{special[X], ⇐, is–trivial–tuple[X]}, {merged[sorted[left–split[X]], 
                                sorted[right–split[X]]], ⇐, otherwise}})})

}, {(Underscript[((Underscript[∀ , is–tuple[
                        X]])), ¬ is–trivial–tuple[X]])∧{({{left–split[X] ≺ X}, {right–split[X] ≺ X}})}, {
}, {(Underscript[((Underscript[∀ , is–tuple[X]])), is–trivial–tuple[X]])(special[X] = 
                    X)}, {(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                          Z]])), ¬ is–trivial–tuple[
                        X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})}})}

then

(Underscript[∀ , is–tuple[X]])is–sorted–version[X,  sorted[X]]

In other words, we found completely automatically that the divide-and-conquer algorithm is a correct sorting algorithm, if we take (or invent) any subalgorithms 'merged', 'left–split', 'right–split'  that satisfy the specifications formulated in the above theorem!

Recent Breakthrough

Recently, I managed to obtain by the above automatic algorithm synthesis method my own Gröbner bases algorithm, see

B. Buchberger. 
Towards the Automated Synthesis of a Gröbner Bases Algorithm.
RACSAM (Review of the Royal Spanish Academy of Science), to appear, 10 pages.

Conclusion

I believe that, going into the direction of systems like Theorema, the following is / will soon be possible:

Computer-support of all aspects of doing mathematics will reach higher and higher levels including inventing, exploring, proving.

In particular, nonalgorithmic and algorithmic mathematics will be supportable in one common logical and software-technological frame.

Mathematical software systems, in addition to providing algorithm libraries, will  have to provide huge mathematical knowledge libraries. Building up and using such libraries, essentially, is a task of formal logic.

The education of mathematicians will have to shift towards including in-depth training on the formal / logical aspects of mathematics.

References

On Gröbner Bases

[Buchberger 1970]
B. Buchberger. Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems (An Algorithmical Criterion for the Solvability of Algebraic Systems of Equations). Aequationes mathematicae 4/3, 1970, pp. 374-383. (English translation in: [Buchberger, Winkler 1998],  pp. 535 -545.) Published version of the PhD Thesis of B. Buchberger, University of Innsbruck, Austria, 1965.

[Buchberger 1998]
B. Buchberger. Introduction to Gröbner Bases. In: [Buchberger, Winkler 1998], pp.3-31.

[Buchberger, Winkler, 1998]
B. Buchberger, F. Winkler (eds.). Gröbner Bases and Applications, Proceedings of the International Conference "33 Years of Gröbner Bases", 1998, RISC, Austria, London Mathematical Society Lecture Note Series, Vol. 251, Cambridge University Press, 1998.

[Becker, Weispfenning 1993]
T. Becker, V. Weispfenning. Gröbner Bases: A Computational Approach to Commutative Algebra, Springer, New York, 1993.

On Mathematical Knowledge Management

B. Buchberger, G. Gonnet, M. Hazewinkel (eds.)
Mathematical Knowledge Management.
Special Issue of Annals of Mathematics and Artificial Intelligence, Vol. 38, No. 1-3, May 2003, Kluwer Academic Publisher, 232 pages.

A.Asperti, B. Buchberger,J.H.Davenport (eds.)
Mathematical Knowledge Management.
Proceedings of the Second International Conference on Mathematical Knowledge Management (MKM 2003), Bertinoro, Italy, Feb.16-18, 2003, Lecture Notes in Computer Science, Vol.2594, Springer, Berlin-Heidelberg-NewYork, 2003, 223 pages.

On Theorema

[Buchberger et al. 2000]
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger. The Theorema Project: A Progress Report. In: M. Kerber and M. Kohlhase (eds.), 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),  A.K. Peters, Natick, Massachusetts, ISBN 1-56881-145-4, pp. 98-113.

On Theory Exploration and Algorithm Synthesis

[Buchberger 2000] 
B. Buchberger. Theory Exploration with Theorema. 
Analele Universitatii Din Timisoara, Ser. Matematica-Informatica, Vol. XXXVIII, Fasc.2, 2000, (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.), ISSN 1124-970X, pp. 9-32.

[Buchberger 2003] 
B. Buchberger. Algorithm Invention and Verification by Lazy Thinking.
In: D. Petcu, V. Negru, D. Zaharie, T. Jebelean (eds), Proceedings of SYNASC 2003 (Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, October 1–4, 2003), Mirton Publishing, ISBN 973–661–104–3, pp. 2–26.

[Buchberger 2004]
B. Buchberger. The Four Parallel Threads of Formal Theory Exploration. Technical Report of the SFB (Special Research Area) Scientific Computing, Johannes Kepler University, Linz, in preparation.

[Buchberger, Craciun 2003]
B. Buchberger, A. Craciun. Algorithm Synthesis by Lazy Thinking: Examples and Implementation in Theorema. in: Fairouz Kamareddine (ed.),  Proc. of the Mathematical Knowledge Management Workshop, Edinburgh, Nov. 25, 2003, Electronic Notes on Theoretical Computer Science,  volume dedicated to the MKM 03 Symposium, Elsevier, ISBN 044451290X, to appear.

[Buchberger 2004]
B. Buchberger. 
Towards the Automated Synthesis of a Gröbner Bases Algorithm.
RACSAM (Review of the Royal Spanish Academy of Science), to appear, 10 pages.