Computational Mathematics
Computational Logic
Symbolic Computation

Invited talk at 
Computer Science Logic 2003
Vienna Technical University
25-29 July, 2003

Bruno Buchberger

RISC
(Research Institute for Symbolic Computation)
Johannes Kepler University
A4040 Linz, Austria
bruno.buchberger@jku.at

Copyright Note:  Copyright Bruno Buchberger 2004.

Copying is granted if the following conditions are satisfied:

- the file is kept unchanged
- in particular, it must include the copyright note
- an e-mail is sent to bruno.buchberger@jku.at

If you use the material in this talk, cite it appropriately.

Computational Mathematics

The Notion

Computational Mathematics (computer mathematics, algorithmic mathematics): 

the part (aspect) of mathematics that aims at establishing algorithms for mathematical problems.

A Common Misunderstanding About Computational Mathematics

The Misunderstanding

Computational mathematics: repeat trivial mathematics very many times on fast machines.

The Appropriate Understanding

Computational mathematics needs more mathematics (deeper theorems with more difficult proofs) than non-computational mathematics.

Example: Problem of Gröbner Bases

Problem:   Given F find G such that Ideal[F] = Ideal[G] and G is a Gröbner basis.

(Why is this problem important?)

First "Construction": Non-algorithmic

G := Ideal[F]     ( := set of all linear combinations of polys in F with poly coefficients.)

Proof is trivial.

Construction is worthless:

Construction involves non-algorithmic "set of all" quantifier.

Second "Construction": Non-algorithmic but more informative

G := set of all polys in Ideal[F] with minimal leading power product.

Proof is easy.

Gives some insight: G is finite (by Dixon's Lemma).

Still, construction is worthless:

-  construction of Ideal[F] is non-algorithmic

-  decision about minimality is non-algorithmc

Third Construction: Algorithmic

Theorem (BB 65):
              G is a Gröbner basis  iff, for all f, g ∈ G, SP[ f, g] reduces to 0 modulo G.

Proof is difficult.

Algorithm for constructing G from F:

-  reduce all SP[ f, g]

-  if a reduction yields h≠0, add h to F.

Partial correctness: an easy consequence of the theorem.

Termination: by Dixon's Lemma.

Two Flavors of Computational Mathematics

Numerical Mathematics

Establishes algorithms that

-  replace the original problems by approximate problems

-  give approximate answers to the approximate problems.

This is often very appropriate because

-  for some problems no algorithm exists

-  for some problems no sufficiently efficient algorithm exists

-  for some problems approximate answers to approximate problems are sufficient.

Exact Computational Mathematics

Exact computational mathematics establishes algorithms that

-  work in the original domain or in isomorphic "algorithmic" representations of the domains

-  give exact answers.

Finding Algorithmic Isomorphic Representations

This may be a challenging - or even unsolvable - problem.

Example: the domain of functions generated from x, +, -, ×, :, π, sin, | |  and constants for the rationals cannot be represented algorithmically (Caviness 81).

Example: the residue class domain of polynomials modulo an ideal was conjectured to be algorithmically unrepresentable (1974) but can be represented using Gröbner bases.

Two Flavors of Exact Computational Mathematics

Discrete Mathematics

The mathematical domains, as they are defined, are algorithmic.

Example: algorithmic graph theory, (some parts of) computational geometry.

Computer Algebra

Computer algebra (algebraic computation, sometimes also called "symbolic computation"):

The mathematical domains, as they are defined, are nonalgorithmic: the objects of the domain are "infinite".

The domains must be represented isomorphically in such a way that the objects become "finitary" ("discrete",...). ("Algebraization").

The representing finitary objects have infinite "semantics".

Example: Risch Integration Algorithm

Domain of real functions: objects are infinite.

The Risch integration algorithm operates on "finitary" terms representing functions and not on the functions themselves.

Example: Arithmetic in Poly Residue Class Domains

The polynomial residue domains modulo ideals: objects are infinite.

The arithmetical operations on these domains work on "finitary" representatives (namely certain polynomials in normal form, which can be algorithmically found via Gröbner bases) and not on the residue classes themselves.

Example: Summation

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, which gives a closed form for "all such" expressions:

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"]]

Note: Finitary representatives of infinite mathematical objects have a "symbolic" flavor (infinite semantics, on the meta-level, ...).

Computational Logic

Mathematical Logic

Mathematical Logic: the mathematical meta-theory of mathematics.

Mathematics: characterized by its method of reasoning.

Hence, mathematical logic is essentially the theory of reasoning.

Computational Logic

The Algorithmic Aspect of Logic

As with any other mathematical theory, one can ask the question of algorithmization for mathematical logic.

Computational Logic ("automated theorem proving", "automated reasoning"): The algorithmic aspect of the mathematical theory of reasoning.

General Algorithmic Theorem Proving

In the most general and strongest sense, reasoning can not be made algorithmic.

The positive aspect: general first-order predicate logic semi-decision procedures (e.g. resolution).

Special Algorithmic Theorem Proving

However, there are many restricted, but still quite general, areas of mathematics, for which provers (or variants of provers) can be established:

-  e.g. decision algorithms for the theory of real closed fields (Tarski, Collins et. al)

- e.g. decision algorithms for boolean combinations of equalities over the complex numbers (by Gröbner bases, Wu, etc.)

- e.g. special algorithms for equational logic, inductive proving, etc.

-  semi-decision, proof checking, interactive computer-supported proving.

A General Direction

Special theorem proving has a big future.

Compare: Nobody would expect that, in a computer algebra system (like Mathematica), one has only one algorithm for "solving"!

One must see all the various areas and aspects of algorithmic theorem proving together.

And one must see them together with computer algebra!  ⟶  Symbolic Computation.

Symbolic Computation

The Notion

Symbolic Computation = Computational Algebra + Computational Logic

+   ...   union, interaction

See editorial of the Journal of Symbolic Computation 1985 (BB et al.).

"Computational Algebra": computational algebra, computational analysis, computational geometry, ...

"Computational Logic": computational logic, computer-aided software development, ...

Viewing the Algorithmization of Mathematics (⊃ Software Science) as One Body

-  the algorithmization of proving, solving, simplifying and their interaction

-  object level and meta-level

-  theory exploration versus isolated theorem proving

Proving, Solving, Simplifying

(Maybe) the Three Basic Mathematical Activities

Given a theory T.

A prover for T:             if it yields "proved" on input E, x  and K,

\(\(\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \)\(∀ \+x 
        E\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ should\ be\ a\ logical\ consequence\ of\ K\ and\ \(\(T\)\(.\)\)\)\)\)

A solver for T:             for input E, x, and K, the output x->t should be such that

\(\(\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \)\(∀ \+y\( 
            E\_\(\(x\)\(←\)\(t\)\(\ \ \ \ \ \ \ \ \)\)\) 
        is\ a\ logical\ consequence\ of\ K\ and\ \(\(T\)\(.\)\)\)\)\)

A simplifier for T:        for input E, x, and K, the output F should be such that

\(\(\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \)\(∀ \+x\ \((E\  ⇔ \ 
            F)\)\ \ \ \ is\ a\ logical\ consequence\ of\ K\ and\ \(\(T\)\(.\)\)\)\)\)

(Computation is a special case of simplification.)

A Rough Assignment

Computational Algebra: algorithmic solvers, algorithmic simplifiers.

Computational Logic:    algorithmic provers.

Future mathematical systems: a library of provers, solvers, simplifiers, which are combined and can be combined in numerous ways.

One of the objectives of the Theorema project.

One of the objectives of the EU Calculemus project / network.

Example: Geometric Theorem Proving by Gröbner Bases in Theorema

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 Proof Automatically Generated by the Theorema Groebner Bases Prover:

Example: Elementary Analysis Proofs by the PCS Method (BB 2000)

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"]}})]

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

The Proof Automatically Generated by the Theorema PCS Prover:

Object Level and Meta-Level

Example: Proving by Gröbner Bases

Object level: Give a proof (hopefully, some day, an automated proof) of the main theorem of GB (the correctness of the GB algorithm, ...).

Jump to the meta-level: Make the GB algorithm an inference rule for automated proving in a special theory.

Example: The Rules of Elementary Analysis

Object level:  (Automatically) prove various lemmata on 'limit':

lim[f + g] = lim[f] + lim[g]

Jump to the meta-level: Make these lemmata inference rules for the simplification of limit expressions:

(lim_(n -> ∞)) (F + 
            G) = (lim_(n -> ∞)) 
          F  +  (lim_(n -> ∞)) G

Note: the first 'lim' is a function, the second 'lim' is a quantifier!

The Significance for Practical Mathematics

The above jump to the meta-level ( = transition from "knowledge" to "inference rules") is one of the reasons why the built-up of mathematics was possible.

Reflection Principle, "Internal Strategies": enormous practical significance.

Theory Exploration versus Isolated Theorem Proving

Isolated Theorem Proving

This is currently the prevalent paradigm in the ATP community, see the annual CADE competitions.

Isolated theorem proving: For a fixed theory T (e.g. the empty theory), test how many and how difficult input statements can be proved how fast.

(Theorem provers, in this paradigm, are considered as black-box "proving engines".)

Mathematical research does not work according to this paradigm.

Theory Exploration

Theory Exploration: For a fixed theory T, and for any initial knowledge base K, systematically help the user building up all "interesting" consequences of K.

The difficulty of (automated) proving crucially depends on which intermediate lemmata one is introducing in which order.

The process of theory exploration is what is in the center of interest of "working" mathematicians. This process is complex:

- it needs creativity

- algorithmic support is possible, desirable, and challenging.

B. Buchberger.
Theory exploration with Theorema.
In: Proceedings of SYNASC 2000, Oct. 4-6, 2000, Timisoara, Rumania, pp. 9-32.

Ingredients and Integration

The process of theory exploration starts from a couple of concepts (functions and predicates) and "complete" knowledge on these concepts.

-  introduce new concepts by axioms (definitions) by using "axiom types"

-  invent new knowledge "bottom-up" by applying "knowledge types" that describe the interaction of the new concepts with the given ones

-- prove / disprove the proposed knowledge

-- in case of failing proofs: invent useful lemmata (apply this recursively)

-  invent problems by applying "problem types"

-- invent algorithms by "algorithm types" and attempt correctness proofs

-- in case of failing proofs: invent specifications for the subalgorithms (apply this recursively).

All these ingredient processes can be / should be automated or, at least, computer-supported.

The Theorema System

Theorema tries to integrate (in the language of predicate logic)

- proving, solving, simplifying (computing)

- the formulation of statements and algorithms

- the structured built-up of knowledge bases

- auxiliary algorithms necessary for the theory exploration process (e.g. analyzers of failing proofs, conjecture generators, libraries of knowledge types, problem types, algorithm types etc.)

- known reasoners (provers, solvers, simplifiers) from other systems and some new reasoners.

Future Mathematical Software Systems

Should be integrated systems combining all above aspects for supporting all phases of "Mathematical Knowledge Management".

MKM 2001 at RISC, MKM 2003 in Bologna, MKM 2003 Birmingham.

Special issue on MKM of AMAI.

MKM network of the EU.

Example: Algorithm Invention by "Lazy Thinking"

Lazy Thinking

"Lazy Thinking": Try various algorithm types, try to prove correctness, analyze failing proofs and guess requirements for the subalgorithms.

Example: Problem of Sorting

Definition

Initialize system!

Definition["is sorted version",any[is–tuple[X],  Y],
is–sorted–version[X, Y]  ⇔(∧{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})} )]

"Complete" Knowledge

Definition["is sorted",\(any[x, y, z\&_]\),
({{is–sorted[⟨⟩] }, {is–sorted[⟨x⟩]}, {\(is–sorted[⟨x, y, 
                    z\&_⟩]\)   ⇔
(∧{({{x ≥ y}, {\(is–sorted[⟨y, 
                                z\&_⟩]\)}})} )}})]

Definition["is permuted version",\(any[x, x\&_, y, y\&_]\),
({{⟨⟩≈⟨⟩ }, {\(⟨⟩ ≉ ⟨y, y\&_⟩\)}, {\(⟨x, 
                    x\&_⟩ ≈ ⟨y\&_⟩\  ⇔ \((x ∈ ⟨y\&_⟩ ∧ ⟨x\&_⟩ ≈ 
                      delete[x, \ ⟨y\&_⟩])\)\)}})]

....

Proposition[\("only empty tuple equivalent to empty tuple", 
      any[is–tuple[
          X]], 
\((X ≈ ⟨⟩)\) \[Implies] \((X = ⟨⟩)\)\)]

...

Dozens of formulae constitute the "complete" knowledge on these concepts. (All these formulae can be proved automatically by Theorema and similar systems. In fact, many of these formulae can also be invented by the lazy thinking paradigm.)

Collect (Relevant) Knowledge in a "Theory"

Theory["lazy thinking correctness of sort",
({{Definition["is sorted"]}, {Definition["is permuted version"]}, {Definition["is sorted version"]}, {...}, {Proposition["only empty tuple equivalent to empty \
tuple"]}, {Proposition["reflexivity of permuted version"]}, {...}})]

The Correctness Theorem for the Unknown Sorting Algorithm "Sorted"

Theorem[\("correctness of sort", 

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

Now Press the Button and a Sorting Algorithm (Various Sorting Algorithms) Will be Invented and Verified Automatically

Call the Invention Cascade

We can now call the lazy thinking procedure by the following call in Theorema:

Prove[Theorem["correctness of sort"], using -> 
            Theory["lazy thinking correctness of sort"], by -> 
            CascadeLT[SqnsEqCasePC,  GenerateConjectures,  nS,  aNS,  
              kConjectures,  nConjectures], built–in -> {Property[≈->{Commutative}]}, \(ProverOptions -> {SqnsProofTechniques -> {"WFInd"}, \ SqnsWFOrdering -> •[ ≻ ], \ 
                GRWTarget -> {"kb", \ "goal"}, \ 
                AllowIntroduceQuantifiers -> True}\), SearchDepth -> 50]//Timing

The generation and verification of the algorithm will take approximately 12 minutes.

Meanwhile we continue with the talk.

Algorithm Type: Divide and Conquer for Tuples

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

The functions 'special', 'left–split', 'right-split', 'merged' are unknown.

The predicate 'is–trivial–tuple' is known: tuples with length ≤ 1. (Definition is part of the knowledge base.)

The Proof Method Attached to the Algorithm Type: induction over the length.

Lazy Thinking: First Round

Proof Attempt (by Automated Prover)

We now attempt to prove

the correctness theorem for the unknown algorithm 'sorted'

using

the knowledge on the concepts in the problem specification

the knowledge on the chosen algorithm type

by

the above inductive proof method.

(Automated) Conjecture Generation from Failing Proof

The proof fails (because nothing is known on 'special', 'left–split', 'right–split', 'merged'.

By considering the algorithm type, the proof naturally splits into two cases:

\(is–trivial–tuple[⟨\(x\_0\)\&_⟩]\)

\(¬ is–trivial–tuple[⟨\(x\_0\)\&_⟩]\)

In fact, the proof already fails in the case  'is–trivial–tuple[\(⟨\(x\_0\)\&_⟩\)]'.

However, amazingly, from the failing proof the following requirement on 'special' can be generated (automatically):

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

Note: This requirement on 'special' is not some strange condition but is simple and natural.

Return to (the Beginning of) the Main Proof

Lazy Thinking: Second Round

Proof Attempt (by Automated Prover)

We now attempt, again, to prove

the correctness theorem for the unknown algorithm 'sorted'

using

the knowledge on the concepts in the problem specification

the knowledge on the chosen algorithm type

the requirement generated in the first round:

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

by

the above inductive proof method.

(Automated) Conjecture Generation from Failing Proof

The proof fails again (because nothing is known on 'left–split', 'right–split', 'merged'.

This time, the proof fails in one of the branches in the case  '¬is–trivial–tuple[\(⟨\(x\_0\)\&_⟩\)]'.

However, amazingly, from the failing proof the following requirement on 'special' can be generated (automatically):

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

Note: This requirement on 'left–split', 'right–split', 'merged' is not some strange condition but is simple and natural.

Return to (the Beginning of) the Main Proof

Lazy Thinking: Third Round

Proof Attempt (by Automated Prover)

We now attempt, again, to prove

the correctness theorem for the unknown algorithm 'sorted'

using

the knowledge on the concepts in the problem specification

the knowledge on the chosen algorithm type

the requirements generated in the first and second round:

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

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

by

the above inductive proof method.

(Automated) Conjecture Generation from Failing Proof

The proof fails again (because too little is known on 'left–split', 'right–split', 'merged'.

This time, the proof fails in the last branch in the case  '¬is–trivial–tuple[\(⟨\(x\_0\)\&_⟩\)]'.

However, amazingly, from the failing proof the following requirement on 'special' can be generated (automatically):

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

Note: This requirement on 'merged' is not some strange condition but is simple and natural.

Return to (the Beginning of) the Main Proof

Lazy Thinking: Last Round

Proof Attempt (by Automated Prover)

We now attempt, again, to prove

the correctness theorem for the unknown algorithm 'sorted'

using

the knowledge on the concepts in the problem specification

the knowledge on the chosen algorithm type

the requirement generated in the first and second round:

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

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

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

by

the above inductive proof method.

This Time the Proof Goes Through Successfully

What Do We Know at the End?

We know now ...

that the algorithm

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

is a correct sorting algorithm, i.e. satisfies the correctness theorem

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

if we take, as subalgorithms, any algorithms 'special', 'left–split', 'right–split', 'merged' that satisfy the following "requirement" (i.e. problem specification):

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

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

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

(and respect types).

Note: This theorem was invented and proved completely automatically.

How Can We Proceed?

The subalgorithm 'special' is fully described by the requirement.

We can now look in our knowledge base for algorithms 'left–split', 'right–split', 'merged' that satisfy the above requirements.

Note: Future mathematical software systems must be mathematical knowledge bases, not only algorithm bases!

If we find such algorithms then we are done.

If we do not yet have such algorithms 'left–split', 'right–split', 'merged' in our knowledge base then we can apply the lazy thinking method again for inventing and verifying such algorithms.

The Whole Cycle Could be Repeated Now With Other Algorithm Types

Then we would get various different sorting algorithms.

The Algorithm Synthesized by Theorema Can Also Be Executed within Theorema

Compute[sorted[⟨⟩]]

Compute[sorted[⟨555⟩]]

Compute[
      sorted[⟨1, 233, 3, 44, 5, 66, 7, 
          8⟩]]

Summary

The algorithmization of mathematics on the object and the meta-level
should be conceived as one integral endeavor.

It fulfills the age-old aspiration of mathematics
towards efficient problem-solving by deepened knowledge.

Appendix: The Four Notebooks Automatically Generated During the Synthesis of Merge-Sort

First Notebook

Pending proof of (13.4).

Pending proof of (8).

Second Notebook

Pending proof of (41.4).

Third Notebook

Fourth Notebook