Theorema 2.0
Theorem Proving
in
Mathematica

Wolfgang Windsteiger
Research Institute for Symbolic Computation (RISC)
JKU Linz, Austria


Wolfgang.Windsteiger@risc.jku.at

http://www.risc.jku.at/research/theorema/software/

What is Theorema?

A Mathematical Assistant System that supports and facilitates all aspects (or at least: as many as possible) of the work of a mathematician:

formulation of theorems and entire bigger theories of knowledge,

(conjecture new statements,)

prove (conjectured) statements,

design and implement algorithms,

execute algorithms / perform computations,

present mathematics in papers / talks / …

…

The “pencil and paper of the (21^st) century.

Conceived, initiated, and also implemented by Bruno Buchberger ∼1995.

Developed by the Theorema Group at RISC (since then, until ∼2006).

Major re-launch (re-design & re-implementation) since ∼2010: Theorema 2.0 (mainly by WW).

Available under GNU GPL Version 3 (since June 2014).

Realization of Theorema / System Architecture

Implemented in Mathematica, available as Mathematica package.

Emphasis on user interface ⟶ heavy use of dynamic user interface elements from Mathematica.

User interface: Notebooks + Theorema Commander

Notebooks:

Carry mathematical content.

Appear like “normal” mathematical documents (papers, lecture notes, books, etc.).

Mathematica notebooks with specialized style sheet in order to correctly process formal parts (definitions, theorems, etc.) contained in the notebook.

Theorema Commander:

Assists in inputting mathematical content.

Assists in performing actions on the mathematical content.

Hides all calls to Theorema-package functions in the GUI ⟶ not a single Theorema-command can be used via the usual command[…]-syntax.

System Demo

Writing Mathematics in Structured “Environments”

Using Mathematical Knowledge (Part I): Computation

Note, that in order to use the definitions they need to be “activated” in the commander.

This compares to the standard Mathematica polynomial multiplication …

Expand[(4+5/2x+23/4(x^3))*(11+1/3x)]

Generating Automated Proofs

The statement we want to prove is the following:

“If the composition of two functions is surjective, then the outer one must be surjective, too.”

Introducing the Concepts

Auxiliary Knowledge

We state the theorem for fixed functions v and u assuming u:X->Y and v:Y->Z.
The only knowledge we need in this proof (apart form the definitions) is the following:

Stating the Theorem & Giving a Proof

Some Comments on the Generated Proof

Every logical step is explained in English (language configurable!).

Granularity of explanation configurable.

Proof search tree and proof explanation notebook are bi-directionally interlinked.

Proof generation info from GUI is displayed in the notebook, so that results are reproducible. Necessary info is stored in auxiliary files, not in the notebook.

Substitution is used quite intelligently (in terms of “automated reasoning): we have the equality

and we use it to substitute b by (v∘u)[a], which is “right to left” in this case. What we do in general is to use both directions, the first one that applies “wins” and blocks the reverse direction.

We have deactivated the rule “Instantiate meta-veriables by matching” because this way we get a “nicer proof”, i.e. it shows the application of unification, which I want to demo in this example.

Where to Go from Here?

Bring in more provers that we already had in Theorema 1 (set theory, induction, ϵ-δ-proofs from elementary analysis, etc.).

Use the system in math education

Use the system in formalization of mathematically interesting areas (e.g. auction theory in theoretical economics, e.g. Vickrey’s theorem on second-price auctions)

Availability

Theorema 2.0 is available under GPL available from the Theorema Homepage and/or GitHub.

http://www.risc.jku.at/research/theorema/software/

https://github.com/windsteiger/Theorema