TH∃OREM∀
and 
Mathematical Knowledge Management

Bruno Buchberger
RISC 
(Research Institute for Symbolic Computation)
Johannes Kepler University, Linz, Austria
Bruno.Buchberger@RISC.Uni-Linz.ac.at

Talk at the IMA Workshop "Special Functions in the Digital Age"
August 1, 2002, University of Minnesota,Minneapolis, USA

Copyright Note: Copying is permitted under the condition that 
- the file is kept unchanged 
- in particular, the copyright note is included, and
- a note is sent to buchberger@risc.uni-linz.ac.at

The Simple Message

Summary

Function Tables are Mathematical Knowledge.

Function Tables are "Digitized".

There is Lots of Mathematical Knowledge Other Than Function Tables.

All Mathematical Knowledge should be "Digitized".

"Function Tables" (Formulae Handbooks)

Example:

(∑_(k=1,…,n))(((-(((-1))^k) (2^(-2 k)) (2 k)! (1+4 k))/(k! (1+k)! ((-1)+2 k))))=1+((-(((-1))^n) (2^(-2 n)) (2 n)!)/(n! (1+n)!))

See: P.Paule, Computer-Solution of Problem 94-2, SIAM REVIEW Vol.37 (1995),105-106.

This is a "formula": equality, inequality, ...  with a couple of free variables.

What Does "Digitized" Mean for Function Tables ?

Basic Meaning:

Formulae accessible (over the web) in some machine-readable text format (TeX, MathML, etc.).

Hard enough!

Extended Meaning I:

Formulae can be used (evaluated, applied for simplification of other formulae, etc.) applying certain (simple, ...) algorithms.

Example: Integral tables as part of integration "algorithm" in math systems like Macsyma, Maple, Mathematica, etc.

Extended Meaning II:

Formulae (from a certain infinite class) can be invented and / or proved by an algorithm.

Such algorithms (like Risch' algorithm for integration, or Gosper-Zeilberger-Paule-... method for summation) are based on mathematical theorems that go beyond the content of the formulae to be invented / verified.

Such algorithms are based on "meta-theorems".

Over the past decades, tremendous progress has been made in the mathematics on which the algorithmic invention / proof of formulae in "funtion tables" is based.

General Mathematical Knowledge

The Class of Predicate Logic Formulae

Mathematical knowledge is much more than the formulae contained in math tables and handbooks.

As a matter of fact, all mathematical knowledge can be (conveniently) formulated in predicate logic:

limit[f, 
        a]⟺ (Underscript[((Underscript[∀ , ϵ])), ϵ > 0])(Underscript[∃ , N])(Underscript[((Underscript[∀ , n])), n ≥ N])\[LeftBracketingBar]f[n] - 
                  a\[RightBracketingBar] < ϵ

is–topology[
          P, 𝒰]⟺
∧{({{(Underscript[∀ , p ∈ P])(Underscript[∀ , N ∈ 𝒰[p]])N∈P
}, {(Underscript[∀ , p ∈ P])(Underscript[∀ , N ∈ 𝒰[p]])p ∈ N}, {(Underscript[∀ , p ∈ P])(Underscript[∀ , M ∈ 𝒰[p], 
                      N ⊆ P])(M ⊆ 
                        N  \[Implies] 
                      N ∈ 𝒰[
                          p])
}, {(Underscript[∀ , p ∈ P])(Underscript[∀ , M, N ∈ 𝒰[p]])M ⋂ 
                      N∈𝒰[
                      p]
}, {(Underscript[∀ , p ∈ P])P∈𝒰[p]
}, {(Underscript[∀ , p ∈ P])(Underscript[∀ , M ∈ 𝒰[p]])(Underscript[∃ , N ∈ 𝒰[p]])(Underscript[∀ , n ∈ N])M ∈ 𝒰[n]}})}

(Underscript[∀ , F ⊆ 𝒫])(Underscript[∃ , G ⊆ 𝒫])((Ideal[F] = Ideal[G]) ∧ 
            is–Groebner–basis[G])

In general, formulae expressing mathematical knowledge may contain quantifiers (∀, ∃, ...).

Typically, formulae in math tables and handbooks are quantifier-free. (What about the Σ-quantifier ?)

The Fundamental Interplay Between Quantifier Math and Quantifier-Free Math

The part of mathematics that can be expressed by quantifier-free predicate logic is the "symbolic computation" part of mathematics. ("High school" proving, "manipulation" of formulae by "transformation", substitution and replacement, ...)

It contains "programming and computation" as a special case.

Mathematics in "non–algorithmic", "abstract" domains typically starts with formulae that contain quantifiers.

Example: definition of limit:

limit[f, 
        a]⟺ (Underscript[((Underscript[∀ , ϵ])), ϵ > 0])(Underscript[∃ , N])(Underscript[((Underscript[∀ , n])), n ≥ N])\[LeftBracketingBar]f[n] - 
                  a\[RightBracketingBar] < ϵ

The first steps in the exploration of a mathematical notion (whose definition involves quantifiers) aim at proving theorems on the interaction of the new notion with known notions that can be expressed quantifier-free.

Example:

limit[f, a] ∧ 
      limit[g, b]⟹limit[f + g, a + b]

The proof of these theorems needs full quantifier-logic.

In contrast, the application of these theorems, only uses quantifier-free logic ("symbolic computation").

In other words, the goal of mathematical exploration is

to prove by quantifier-logic

quantifier-free formulae

about notions defined in quantifier-logic

in order that, in the future, the application of these theorems can proceed quantifier-free.

What Does "Digitized" Mean for General Mathematical Knowledge ?

Basic Meaning:

Formulae accessible (over the web) in some machine-readable text format (tex, MathML, etc.).

See, for example, the MathWorld project by Eric Weisstein accessible via the Mathematica web site.

(Note: "Basic" does not mean "useless" nor "effortless".)

Extended Meaning I:

Formulae can be used (retrieved, compared, evaluated, etc.) applying algorithms.

Example:

Given: A definition of "topology" in a slightly different formulation and notation.

Question: Is this definition "contained" in a given knowledge base, i.e. is this definition equivalent with the one in the knowledge base?

In the context of general math knowledge, these goals are not easy to achieve:

Essentially, the algorithmic solution of these questions needs automated theorem proving (both  in quantifier-free and quantifier-logic).

Extended Meaning II:

Formulae (from a certain infinite class of quantifier logic) can be invented and / or proved by an algorithm.

There are theorem proving algorithms

for the class of all predicate logic formulae (e.g. Robinson's resolution method)

for various special classes (formulae in special "theories"), e.g. the theory of reald closed fields (Collins' algorithm).

As in the case of function tables, such algorithms are based on "meta-theorems".

(The formulae in function tables are a special class of math formulae).

Mathematics can be viewed as a network of meta-theories: A theorem on a meta-level may "trivialize" the invention / proof of infinitely many theorems on the object level.

Tremendous progress in "trivializing" the invention / proof of "formulae" has been made in the past few decades.

(The algorithms for inventing / proving certain classes of formulae in function tables are one example of such trivializing algorithms. Others are Collins' algorithm for the theory of real closed fields or the Groebner bases method for geo proving.)

The trivialization of the invention / proof of a particular (infinite) class of formulae, typically, is a highly nontrivial task.

Ingredients of Future "Digitized" Mathematical Knowledge Management Systems

One Logic Frame

Formulae must be expressions within a formal language / logic  and not only "texts".

Preferrably, there should be one uniform logic frame for all of mathematics.

Predicate logic is a natural candidate for such a universal logic frame.

(If we allow various logics, mutual translation  / interpretation must be provided.)

Math Knowledge Bases

All mathematical knowledge must be formalized within this language / logic frame.

By Bourbakism, one knows that (even first order) predicate logic is a suitable language for all of mathematics.

In fact, predicate logic is also a convenient and elegant language.

(Side remark: Strangely enough, practically, the Bourbaki volumes are not good examples of well formalized texts!)

(Side remark: The formal abilities and the formal culture of (some,many, ...?) current mathematicians are not mature enough for this goal.)

Proving, Solving, Simplifying (Computing)

These are the key activities of mathematics.

They must be expressible in one logic / system frame.

Predicate logic is a natural frame for these three aspects.

Current systems do not integrate the three aspects.

Structured Knowledge Bases

The key to success in mathematical exploration is to proceed in exploration layers.

One exploration layer:

Given notions and knowledge about these notions.

A new notion is introduced by describing its relation with the given notions (definitions, axioms).

Exploration of new knowledge: All the possible interactions of the new notion with the given notions and with itself are explored by proving and added to the knowledge base.

Termination criterion: new knowledge is "complete" when all other consequences can be proved by quantifier-free logic.

Example:

(gcd[x, y] | x)  ∧ (gcd[x, y] | 
          y) ∧ (Underscript[∀ , z])((z | x ∧ z | 
                  y)⟹z | gcd[x, y])

Such axioms define a "functor" that describes a new domain (with operation "gcd") in dependence on a given domain (with operation "|").

A functor does not only map operations into operations but also properties of operations in to properties of operations.

Automated Proving, Solving, Simplifying

The core of future Mathematical Knowledge Management Systems:

knowledge bases for various theories

libraries of algorithmic provers, solvers, simplifiers for many theories

facilities for extending existing provers, ... and for programming new provers, ...

Formula Retrieving = A Special Case of Proving

A formula is retrievable from a knowledge base if it is "easily" provable from the knowledge base.

Current "Digitized" Mathematical Knowledge Management Systems

There are basically no systems that have all the above ingredients:

function tables etc: confined to quantifier-free knowledge

"math software systems" like Mathematica, Maple, ...: no proving

proof checkers like Mizar: no automated proof generation (Mizar is the only system with a huge knowledge base)

automated theorem proving systems like Otter: no solving, programming and computing, no knowledge bases.

September 2001: 1st International Conference on MKM at RISC. European Consortium for MKM formed.

July 2002: North American Conference on MKM at McMaster U, Canada. US Consortium for MKM formed.

February 2003: 2nd International Conference on MKM in Bologna.

Theorema

An attempt at a math knowledge management system with all the above ingredients:

full predicate logic as the language / logic frame,

programmed in Mathematica, i.e. platform-independent; however, does not use implicit knowledge of Mathematica,

heavily uses the Mathematica front-end,

implements a growing library of  new and known methods for computer-supported proving, solving, simplifying for various areas of mathematics,

Theorema Group:  Bruno Buchberger (project leader).
Senior researchers: Tudor Jebelean, Wolfgang Windsteiger, Temur Kutsia, and Koji Nakagawa,
Current PhD students: Markus Rosenkranz, Florina Piroi, Adrian Craciun.
Former PhD students: Elena Tomuta, Daniela Vasaru, Claudio Dupret.

Example: Manipulating Mathematical Text

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

Definition["limit:"] // InputForm

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: Some Provers

Example: The PCS Prover

A heuristic proof method (BB 2000) for predicate logic, in particular, for formulae with "alternativing quantifiers".

Generates "natural" proofs.

Reduces proving to solving.

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

Proof contains interesting algorithmic and didactic information!

Such proofs seem to be trivial but they are a challenge for automated proving.

Proof generated completely automatically by the above prover algorithm (PCS) call:

Example: Set Theory Prover

The Theorema set theory prover (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])\)\)]

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]

Proof generated completely automatically by the above set theory prover call:

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

Failing proof:

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

The above prover call generates a failing inductive proof.

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

The above prover call generates a "cascade" of proofs attempts and proofs. Form the failing proof attempts, a "conjecture generator" generates conjectures for lemmata whose proof leads to a successful inductive proof of the main theorem. Here are the five proof attempts and proofs generated in this example:

Proof attempt of theorem and generation of first conjecture:

Pending proof of (1).

Pending proof of (18).

Proof of first conjecture:

Proof attempt and generation of second conjecture:

Proof of second conjecture:

Proof of theorem:

Example: Proving Booleans of Equalities by Groebner Bases

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]

Note: thousands of (interesting and partly unknown) theorems in (coordinate geometry) can be proved by the Groebner bases (and similar) methods: E.g. Pappus Theorem, Desargues Theorem, ...

The above prover call generates the following proof completely automatically. This proof contains also an explanation of the Groebner bases proof method:

Example: Inventing and Proving Σ-Terms

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"], 
transformBy -> Identity, TransformerOptions -> {}]\)

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

See also talk by Carsten Schneider (PhD thesis, advisor: Peter Paule): implements and significantly extends Karr's method.

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]

This instruction calls the Otter prover as an external prover and displays the lines of a resolution proof in an extra window.

Example: Computation Using Functors

A Sparse Polynomials Functor

This definition describes the functor that generates from an arbitrary domain of coefficients C and an arbitrary domain of "power products" (multiplicative terms) T the domain of polynomials over C and T:

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 a special class of predicate logic formulae!

Generate 3-Variate Polys over the Integers

The following sequence of Theorema instructions generates the domain of 3-variate polys over the integers and allows to compute with these polys.

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["quotient field"]}, {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"]⟩]

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 (by the meta-level principle) including inventing, exploring, proving.

In particular, nonalgorithmic and algorithmic mathematics will be supportable in one common logical and software-technological frame (in other words, mathematics, and computer science will reconcile).

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. Hence, computer-supported derivation of theorems from knowledge bases will be a future key tool.

For building up and maintaining such mathematical knowledge libraries, an international consortium  is necessary ("Bourbaki Project in the Digital Age").

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