Wolfram Library Archive

All Collections Articles Books Conference Proceedings
Courseware Demos MathSource Technical Notes
Title Downloads

Computer-Supported Mathematical Theory Exploration

Bruno Buchberger
Organization: Johannes Kepler University
Department: RISC-Linz
Revision date


This notebook discusses possible future ingredients of math systems. Various aspects and demonstrations of Theorema are given, including proofs in set theory, PCS, Pappus' Theorem, Functors, Groebner bases, and Automated Algorithm Invention.

I believe that, going into the direction of systems like Theorema, the following will soon be possible:

Computer-support of all aspects of doing mathematics will reach higher and higher levels including inventing, exploring, proving.

In particular, nonalgorithmic and algorithmic mathematics will be supportable in one common logical and software-technological frame.

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.

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

*Mathematics > Foundations of Mathematics
*Mathematics > Foundations of Mathematics > Set Theory
*Mathematics > Geometry > Plane Geometry

Theorema, Automated Theorem Proving
Related items

*Computer Supported Mathematical Theory Exploration: A Shift of Paradigm in Mathematical Software   [in Conference Proceedings]

Downloads Download Wolfram CDF Player

Buchberger-Theorema-Talk-2004-01-26-12h.nb (875.2 KB) - Mathematica Notebook [for Mathematica 5.0]