The meeting was an attempt to bring together people from different communities: constructive algebra, computer algebra, designers and users of proof systems. Though the goals and interests are distinct, the meeting revealed that there is a strong core of common interests, the main one maybe the shared desire to understand in depth mathematics concepts in connections with algorithms and proofs. An interaction appears thus to be possible and fruitful. One outcome of this week was the decision to create a European group under the acronym MAP for "Mathematics: Algorithms and Proofs". As we said in our proposal: "If there is enough common interests and good interactions during the week, the Dagstuhl seminar could be the starting point of a european proposal on the same topic, with more ambitious goals." This is indeed what happened.

We would like at this point to thank the team of Schloss Dagtuhl. The exceptional working conditions we enjoyed there played an important rôle in the success of the meeting.

Here are some common themes that emerged in the meeting on constructive algebra and verifications. There is no attempt to be exhaustive.

• Certificates
  A first common theme that emerged can be captured by the notion of "certificate", and was exposed clearly by the talk of Arjeh Cohen. This notion unifies some attempts to connect proof systems and computer algebra systems, that were the topic of the talks of Loic Pottier and David Delaye. The idea is roughly that computer algebra should communicate mathematical data together with a certificate , which represents the information needed to complete a proof of correctness of the mathematical data. This notion is reminiscent of the difference NP/P: it may be hard to check that a formula is a tautology but it is easy to check a proof. A simple example is provided by the gcd of two polynomials P and Q. The computer system should communicate not only the answer G, but also a certificate, that may be four polynomials A,B,C,D such that AP+BQ = G, P=CG, Q=DG. To find G may be hard, but to check these equalities is easy. A more sophiscated example was the topic of the talk of Loic Pottier (special cases of quantifier eliminations for reals), who had to program in CAML his own version of a computer algebra algorithm in order to get the desired certificates. This notion of certificate is also closely connected to the talk of Helmut Schwichtenberg (common to all interactive proof systems with explicit proof objects): a starting point of such work is that while it is undecidable in general whether a given program meets its specification. In contrast, it can be checked easily by a machine whether a formal proof is correct. The proof object itself can thus then be used as a certificate. It is curious that a similar notion of certificate was used in the talk of Dmitrii Pasechnik. There, of course, the goal is completely different, which is to provide interesting strong propositional proof systems with lower bound results. Finally, the talk of Laureano Gonzalez-Vega was concerned on the difficulty of computing algebraic certificates in some geometrical statements in Real Algebraic Geometry.
• Algorithms in Mathematics, via Proof Theory
  A second theme is what one may call the relevance of classical mathematics to algorithms. The talks of Henri Lombardi, Marie-Francoise Roy and Ulrich Kohlenbach showed, in very different ways, that mathematical proofs that use a priori highly non computational concepts, such as Zorn lemma, or compactness principles, contain implicitely very interesting computational informations. The talk of Ulrich Kohlenbach presented a way to extract implicit informations in proofs, in such a way that one can even obtain new theorems, surprising to the expert, from these informations (here in the field of metric fixed point theory). One interesting topic is to compare the two approaches: in Lombardi and Roy's talks, to use techniques from geometric logic, and in Kohlenbach's talk, a modification of Gödel's dialectica interpretation, that is especially well suited to extract bounds from classical proofs. Ulrich Kohlenbach said for instance that it should be interesting to use his methods also for examples on algebra, where the dynamical method of Lombardi-Roy has been used so far. A general feeling, emerging from some talks and discussions, was that the algorithms extracted by the dynamical method from a priori non effective proofs, may give algorithms that are better (even feasible) than the algorithms one can extract more straightforwardly from usual constructive arguments. For instance, in usual constructive mathematics, one requires to have a test of irreducibility for polynomials. While such a test exists in some cases, there are usually quite inefficient. The algorithm corresponding to a proof using this test is thus a priori also inefficient. By contrast the algorithm extracted from dynamical methods does not rely on such tests. It was suggested by Henri Lombardi that some efficient algorithms may be obtained in this way in number theory (dynamical theory of Dedekind domains). Such claims, if they happen to be verified, are of fundamental importance.
• Progress on basics
  Another theme is best expressed by one sentence taken from the presentation of the seminar: "It is remarkable that in constructive and computer algebra, progress in sophisticated algorithms often implies progress on basics". This point was stressed in the talk of Peter Paule on symbolic summation for instance, who provided basic examples that would be welcome additions to basic courses on calculus, and several time in discussions, for instance for algebraic topology. Another example was provided by the talk of Gilles Dowek, who, motivated by a quite concrete problems in safety of air trafic control, presented a new form of induction over real numbers that may be interesting for presenting basic proofs in real analysis.
• Proof Systems and Computer Algebra Systems
  A large part of the talks were concerned about connections between computer algebra systems and proof systems. Peter Paule reminded us, with some concrete examples, that people in proof system should be more aware of the power of current computer algebra systems. The talks of Renaud Rioboo presented a system aiming at combining proofs and computer algebra computations. The talks of Clemens Ballarin and Julio Rubio supplemented the talk of Francis Sergeraert by presenting an on-going attempt to use techniques from formal methods and interactive proof checking to ensure the correctness of a large sofware system for computations in algebraic topology. One interesting conceptual connection emerged from the talk of Peter Paule, on the concrete example of checking tables of equalities between special functions. But there is a mismatch between this representation and the representation of expressions as functions of real or complex quantities. Typically, the functions may have pôle, or may involve ambiguities. What interest primarily the user of such tables is of course the interpretation of expressions as functions.
  This suggests a natural place where proof systems may complement computer algebra system. Such a connection appeared in the talks of Loic Pottier and David Delaye. The simplest example may be the provided by the equality x\times 1/x = 1. This equality is perfectly valid from the computer algebra viewpoint, since it is interpreted in the field of rational expressions (field of fractions of a polynomial ring). Considered as a function x\longmapsto 1/x has a pôle at x=0 and the proof system will have to generate the condition x\neq 0.
• Constructive Mathematics
  Several talks were given on constructive mathematics. Francis Sergereart presented a way to do algebraic topology constructively, which is actually implemented in common lisp. Peter Schuster presented a constructive definition of the notion of scheme, a basic concept in modern algebraic geometry. There are probably deep connections between this presentation, based on point-free topology, and the talks of Henri Lombardi and Herve Perdry on dynamical algebras, that would be interesting to explore further. The talks of Erik Palmgren and Jesper Carlström were about Martin-Löf type theory. Type theory appears to be a potential formalism in which several concepts that were presented at the workshop could be elegantly expressed. Just to take one example, if we succeed to express constructive algebraic topology, as presented by Francis Sergeraert, in type theory, one would have an algorithm (in a functional programming language) which is correct by construction, thus bypassing the need of a formal verification a posteriori. In the present stage however, this may seem utopic (probably the program obtained in this way would be too inefficient), but this might be an interesting project. The meeting ended by a talk of Bas Spitters on a constructive proof of Peter-Weyl's theorem, and it would be interesting to explore further the algorithmic ideas implicit in this proof.

The main positive surprise of the seminar was that communication is possible, and in fact highly appreciated, bewteen quite distinct fields of mathematics and computer science. One participant expressed for instance his positive surprise to see in the same talk the name of Jean-Pierre Serre, who made fundamental contributions in algebraic topology, and the name of Turing, one of the founder of the mathematical notion of algorithm. The participants were working in different fields, but were all deeply interested in the interconnections between mathematics, algorithms and proofs, and several participants expressed the opinion that this combination of different topics with a strong common interest allows for a rich interaction. What was positive also was the emphasis, common to many talks, that progress in sophisticated mathematics and algorithms often implies progress on basics. This seminar was also a wellcome occasion to have a beginning of a real dialogue between designers and users of proof systems, and specialists in computer algebra and mathematics. Such dialogues have already started in research groups that were represented (Linz, Nijmegen, Paris VI) but the seminar showed new unexpected research directions (proof theory, constructive algebraic topology).

One outcome of this week was the decision to create a European group under the acronym MAP for "Mathematics: Algorithms and Proofs".