September 25 – 30 , 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)

For support, please contact

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
List of Participants

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 the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.