25. – 30. September 2005, Dagstuhl-Seminar 05391

Algebraic and Numerical Algorithms and Computer-assisted Proofs


Bruno Buchberger (Universität Linz, AT)
Shin'ichi Oishi (Waseda Univ. / JST – Tokyo, JP)
Michael Plum (KIT – Karlsruher Institut für Technologie, DE)
Siegfried M. Rump (TU Hamburg-Harburg, DE)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS

Description and aims of the seminar

Recently, a number of problems have been solved by so-called computer-assisted proofs, among them the celebrated Kepler conjecture, the proof of existence of chaos, the verification of the existence of the Lorenz attractor, and more. All those problems have two things in common: first, the computer is used to assist the proof by solving certain subproblems, and second these subproblems are of numerical nature.

There are also any famous results of nontrivial proofs which can be performed automatically by a computer program. For example, Risch's algorithm for integration in finite terms, solution of polynomial systems by Gröbner bases, quantifier elimination and more. Any of those solves a nontrivial mathematical problem which could be quite hard to solve by pencil and paper.

Those algorithms are frequently executed in exact arithmetic over the field of rationals or an algebraic extension field using well known methods from computer algebra. The problems mentioned in the first paragraph are continuous in nature. Tehy can be solved by so-called verification or self-validating methods.

Basically, self-validating methods verify the validity of assertions of certain theorems which are formulated in such a way that validation is possible by means of numerical computations. The main point is that this validation is absolutely rigorous including all possible procedural or rounding errors. On the one hand, the use of finite precision arithmetic implies very fast calculations, but on the other hand it limits the scope of applicability.

In contrast, most algorithms in computer algebra are 'never failing', that is they are proved to provide a solution for any input, and the maximum computing time for this is estimated a priori. To speed up practical implementations, also hybrid methods combining computer algebra with numerical verification methods are used.

Self-validating and computer algebra methods aim on the reliable solution of certain mathematical problems with the aid of computers. This seems a very natural task. Other areas such as computer geometry and graphics, real number theory, automated theorem proving and more have similar aims. Therefore we think it is very fruitful to create a link of information between experts in those different fields. The common basis or goal is the computer-assisted solution of mathematical problems with certainty.

The choice of organizers also reflects different fields of interest and expertise. The stimulating atmosphere in Dagstuhl was definitely a very fruitful environment for this enterprise.

Related Dagstuhl-Seminar


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.