This is a passionate plea for the proof:

**Forever, in infinite many cases**

A proof is the lazy brain's best friend - it prevents it from the need to test a theorem, a transformation, a change, a program…in finite many, but many!, cases. A proof says: correct in infinite many cases. From "now" on the semantics is functional not necessarily operational.

A proven theorem can be pushed into the knowledge base and used as black box. It becomes a validated building block of the innovative mathematical spiral.

**Mathematical thinking**

**When we want to solve 3*x=5, we may be aware that rational numbers, under multiplication, (Q,*) form an Abelian group and each number is a basis for all others. To solve the equation, we use an equivalence transformation to get a basis that has nice properties for finding the solution:**

3*x=5-->3/3*x=5/3-->x=5/3.

We apply the same principle if we want to solve a system of linear equations. Again, it's a helpful view to see the "unknowns" as weights for column vectors linearly combing the "goal vector".

Provided m=n and the column vectors build a basis (they are linearly independent) a unique solution exists. Again, we use equivalence transformations to get a basis with nice properties…In the matrix language it's a triangular matrix…The core of the proof is the general principle of constructing the bases.

What about a system of multi-variate polynomial equations? The Austrian mathematician Bruno Buchberger has shown that the same principle can be applied…proven by constructing the Gröbner Bases. In short, it transforms the system in a way that one basis element is only univariate.

Deep knowledge in ring theory, ideals…is required.

**Algorithm generators**

**One of Bruno Buchberger's research project is Theorema. In short, automated theorem proving, with a system built atop Mathematica. If the Theorema software can automatically create a constructive proof for the solution of polynomial equations (by constructing Gröbner Bases) it generates the solver.**

This is not required here, because GBs are already constructed. But, in general an automated theorem prover can become an algorithm generator.

**Symbolic computation**

The original objective of this field was

- automating mathematics (not only computation)
- empowering computer science with mathematical thinking and techniques

Remember, the term abstract data type can be regarded as a generalized approach of algebraic structures (lattices, rings, modules..), if you want it's a cousin of the "universal algebra" - a set of elements, a set of operations and a set of rules.

But, without a concrete model and implementation it remains "abstract nonsense".

What we finally want? A language to program everything? The Wolfram Language and its implementation, Mathematica, are really great, but there's still a lot to do - implementing (correctly) what can be described in the language.

There is no such thing as an abstract program. Give me constructive proofs! A Kingdom for a constructive proof!