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.