This seminar is the continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 january 2003.

The goal of the seminar is to bring together people from the communities of formal proofs, constructive mathematics and computer algebra (in a wide meaning).

One objective of the seminar is to bridge the gap between conceptual (abstract) and computational (constructive) mathematics, by providing a computational understanding of abstract mathematics.

It is becoming clear that many parts of abstract mathematics can be made constructive and even computational and that abstract mathematics techniques contains an underlying constructive content.

We are not only interested in algorithms however, but also in formal proofs of the correctness of these algorithms.

Computer algebra provides a variety of interesting basic algorithms, from exact linear algebra to various aspects of elimination and real root counting, which are the foundations for much more sophisticated results like nullstellensatz, quantifier elimination etc... It is remarkable that in constructive and computer algebra, progress in sophisticated algorithms often implies progress on basics.

Moreover the scope of computer algebra is now widened by the consideration of seminumerical algorithms. When such algorithms are correctly controlled, they actually deal with real and complex numbers in the constructive meaning of these objects. So computer algebra is lead to fill many objectives of computational analysis.

Providing formal proofs of correctness to the computer algebra community is very useful, specially for algorithms which are basic and used everywhere.

On the other hand, a collection of mathematically non trivial examples is very useful for the formal proof community, which needs also powerful automatic methods from computer algebra.

We observe that the Dagstuhl seminar 03021, which seems to have been the first meeting devoted to the topic, was a success and has been very satisfactory for the participants. They decided to create a group under the acronym "Mathematics, Algorithms, Proofs". We have organised a similar meeting in Luminy, january 2004, and besides the next Dagstuhl meeting, we are trying to organize a MAP summer school in September 2005 in Santander (Spain).

Since the whole field is rather big, we think that it may be indeed a good idea to choose a focal topic. A good such topic for the next 2005 topic appears to be.

General Presentation

This seminar was the third MAP meeting, a continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 January 2003. The goal of these meetings is to bring together people from the communities of formal proofs, constructive mathematics and computer algebra (in a wide meaning). The special emphasis of the present meeting was on the constructive mathematics and efficient proofs in computer algebra. We were honored to have as invited speakers Helmut Schwichtenberg, proof theorist who is now working on extraction of programs from proofs, Harold Edwards, specialist of the work of Kronecker, and Fred Richman, the specialist of constructive algebra. A sub-theme was on formalization of mathematics, especially on the flyspec project, lead by Thomas C. Hales, and we were fortunate that most people working on this, in particular, besides Hales himself, Jeremy Avigad and Robert M. Solovay were present at the seminar.

Once again, we would like to thank the team of Schloss Dagsthul. The exceptional working condition we enjoyed there played an important part in the success of this meeting.