Subject of the Panel Discussion: Challenging Mathematical Problems (for details see also http://www.ags.uni-sb.de/~calculemus2002/panel/) Panel Members: James H. Davenport, Jvrg Siekmann, Jacques Calmet, Thomas Sturm, Alain Colmerauer, Claude Kirchner Chair: Jacques Calmet Format: 5 minute opening remarks for each panel member, followed by an hour of general discussion, open to the floor. Initial Statements ------------------ Jacques Calmet opened the panel session by arguing that algebraic topology is a field in which automated theorem proving could be successfully applied and that Jesus Aransay a PhD student currently in Karlsruhe is indeed working on this problem. Jvrg Siekmann objected that the real challenge is not to find the occasional problem we can solve and mathematicians cannot, but instead to find mathematicians who are actually interested in formal proofs and certified computer algebra. He argued that although the field of Theorem Proving is around for more than three decades it has not delivered what it promised. On the other hand Computer Algebra actually occupies a market niche, however, its users are generally content with the (buggy) way it currently works. Claude Kirchner replied that it is in particular a problem of the techniques used in theorem proving that are already difficult to relate to anyone inside the field let alone to a user from outside. CASs usually work very intuitive, ATPs not. Moreover, CASs solve hard problems which are difficult even for trained mathematicians whereas theorem provers solve relatively trivial problems in a domain where mathematicians think they are better anyway. Thomas Sturm presented his point calling himself "somewhat of an outsider to the Calculemus community". He claimed that their own work on RedLog is taken seriously by mathematicians and is very much related to automated reasoning aspects. In particular the challenging problem he is proposing (for more details at http://www.fmi.uni-passau.de/~sturm/activities/calculemus/challenge/) would benefit from combined techniques from quantifier elimination, reasoning and computer algebra. James Davenport argued that a combination of theorem proving and computer algebra could very well be attractive for mathematicians. Not only can it provide more reliability but it can in particular give more insights into the problems. Mathematicians (as well as many Engineers) are not only interested in solutions but also into details what the problem entails. Alain Colmerauer commented that instead of trying to become attractive for mathematicians the field should rather try to offer its services to computer scientists and concentrate on verification and design of logical programming languages. Open Floor Discussion --------------------- The discussion focused mainly on the point if mathematicians can be attracted by automated reasoning and if there is a user community for computer algebra systems that contain formal reasoning. Some points of the discussion were: James Davenport emphasized that the work by Wiedijk/Beeson and by Colton presented at Calculemus were the right way to bring both reasoning and notions of formality into CAS. Jvrg Siekmann added that the recent work by Freek Wiedijk in comparing deduction system by applying them to the problem that SQRT(2) is irrational was very impressive and shows how far the field is. Thomas Sturm, however, pointed out that this result should not be overemphasized since if it were advertised as state of the art of the field it might rather turn off mathematicians instead of attract them. Volker Sorge asked the panelists why many discussions at automated reasoning conferences recently become `soul searching' events. Jvrg Siekmann replied that a field has to question its own assumptions occasionally otherwise it is doomed. The emerging semantic web and the necessity for mathematical knowledge management was identified as one future challenge for the community. In this context Volker Sorge suggested whether it would not be wise to consult members from the database and semantic web community before creating large, possibly naively structured, mathematical knowledge base. Jvrg Siekmann dismissed this as the `hackers argument' claiming that first the mathematical data has to be available. However, this was seen as a rather arrogant stance by several members of the audience, since in particular for databases special techniques, such as indexing, are often tailored to the particularities of the data before knowledge bases are created. As other challenging problems for the community, the discussion identified formal classification problems that are either too large or too tedious for mathematicians, as well as formal verification problems in CAS such as definite integration, problems with branch cuts, etc.