Below, you can download the formalizations of mathematical theories in Theorema 2.0, created by Alexander Maletzky. Each formalization consists of one or more content notebooks (which are actually Mathematica notebooks), together with a bunch of proof files.
Note that this site will be superseded by an official online repository of so-called Theorema Knowledge Archives in the future.
|Reduction Ring Theory||Gröbner bases and reduction rings, together with several elementary mathematical theories (sets, algebraic structures, numbers, tuples, ...).|
|Complexity Analysis||Complexity analysis of Buchberger's algorithm in bivariate polynomial rings over fields, w.r.t. a graded term order.|
The minimal prerequisite for being able to inspect and use the formalizations is to have Mathematica (version 8 or newer)
and Theorema 2.0 installed on your computer.
Theorema 2.0 is completely free and even open-source. You can obtain it from the official website, which also provides detailed information on how to properly install it.
The installation of a formalization is fairly straight-forward. Just follow the steps below:
Once you opened a notebook in Theorema (as described above), you can simply browse through its contents. If you want to inspect the proof of a theorem, just click on the respective "Show Proof" link appearing somewhere below the theorem. After a few seconds, a separate notebook displaying the nicely-formatted proof should pop-up (if not, make sure that you really followed step 3 of the above installation guide).
If a formalization consists of more than one notebooks, one of them, called "Overview.nb", contains some general information about the formalization and its logical structure. Therefore, it is a good idea to have a look at this notebook first.
If you encounter any problems, do not hesitate to contact the author. Normally, the formalizations are maintained and updated to work with the latest version of Theorema.