Аннотация:
In this talk I will give an overview on the main ideas of my “Theorema” approach to mathematics, which reflects my view on mathematics that evolved over my life as a mathematician (“from 17 to 71”):
Mathematics is the “art of explanation”, the art of reducing the complex to the simple. Hence, mathematics is of highest relevance for the “wo-man on the street”.
Mathematics is in the center of the “innovation spiral” that starts from basic research on the nature of nature and goes all the way via technology to economy and welfare. Hence, mathematics is of highest relevance to our society.
Mathematics is the meta-theory of itself. It can explain how we derive new mathematical knowledge and methods from available knowledge and methods. This is possible because mathematics is essentially formal. The application of mathematics to itself, i. e. to the mathematical exploration process, was hardly noticeable until the middle of the 20th century. However, now, we can observe what “application of mathematics to itself” means practically. This will be of highest relevance to the way how we will do mathematics (including software) in the future. As a consequence (semi-) automation of the mathematical exploration process will be of highest relevance to the “working mathematician”.
I think that predicate logic (in some nicely readable two-dimensional — even user-definable — syntax) is the natural frame for providing a version of mathematics that pleases the wo-man from the street, society, and the working mathematicians. And all the effort and attention must go to automating natural reasoning in predicate logic for pleasing everybody with more and more attractive mathematics.
This is the reason why approximately in the middle of the 1990-ies I launched the Theorema Project.
In the talk, I will give an overview on the current state of the project, which — due to my many services for “society” that took lots of my time — is not yet at a stage which is satisfactory. However, I hope I will be able to explain a few highlights and to draw a picture from which the avenues to the future can be guessed. For this, as an example I will show how, within Theorema, the essential point of algorithmic Gröbner bases method can be invented automatically.
Of course, Theorema is just one in a group of research projects that pursue the automation of mathematics. I am very optimistic, nervous, and excited to enjoy the dawn of a new era of mathematics that will put mathematics right into the center of modern society in a tangible, natural, artistic and surprising way.
