Some Considerations on the Usability of Interactive Provers

Andrea Asperti (University of Bologna, Italy)

In spite of the remarkable achievements recently obtained in the field of mechanization of formal reasoning, the overall usability of interactive provers does not seem to be sensibly improved since the advent of the "second generation" of systems, in the mid-eighties. We try to analyze the reasons of such a slow progress, pointing out the main problems and suggesting some possible research directions.

Mechanized Mathematics

Jacques Carette (McMaster University, Canada)

If one were designing an entirely new mathematical assistant, what might it look like? Problems and some favoured solutions are presented.

Can we make Mathematics universal as well as fully reliable ?

Pierre Cartier (Institut des Hautes Études Scientifiques, France)

These are times of change for the mathematical profession and for the practice of mathematics, with, for instance, the advent of powerful computing machinery and the extraordinary immediacy of communication all over the world. If the concept of globalization has any meaning, this is now the time of globalization in mathematics. The pretense of mathematics of being universal can now be made real, and mathematical knowledge be shared by people from many different background. In addition, there are now mechanical help in reasoning, digitization of large parts of the traditional mathematical literature, and amazing amounts of scientific data and problems begging analysis which all help to offer a change in the role of mathematics. Checking proofs by computers is just one of the many new possibilities. A new paradigm is needed to understand a world of TERABYTES, where the frontier between "proof" and "guess" is quite fuzzy. Between "finite" and "infinite", we have to introduce in our axiomatics the world of "very very large".

The Challenges of Multivalued "Functions"

James Davenport (University of Bath, UK)

Although, formally, mathematics is clear that a function is a single-valued object, mathematical practice is looser, particularly with $n$-th roots and various inverse functions. In this paper, we point out some of the looseness, and ask what the implications are, both for Artificial Intelligence and Symbolic Computation, of these practices. In doing so, we look at the steps necessary to convert existing texts into

• rigorous statements
• rigorously proved statements.

The Dynamic Dictionary of Mathematical Functions

Bruno Salvy (INRIA Rocquencourt & MSR-Inria Joint Centre, France)

Mathematical tables have long been used by developers of computer algebra systems. Special functions are implemented in a system using formulas obtained in these tables for the computation of their derivatives, series or asymptotic expansions, numerical evaluation, simplification, integral transforms,... Recently, more and more powerful algorithms have been developed by the computer algebra community, so that nowadays, the flow can be reversed and mathematical tables can be generated automatically for large classes of functions. The gains are obvious: a full automation of the process that reduces the risk for typographical or other errors; more flexibility and extra interactivity for the readers, not only in the navigation, but also in the choice of the actual functions or formulas they need. Our team has started the development of a Dynamic Dictionary of Mathematical Functions focusing on solutions of linear differential equations (available at \url{http://ddmf.msr-inria.inria.fr/}). This development raises several interesting issues. Algorithmic ones obviously, but also more fundamental ones (what exactly is needed to define a function?), or practical ones (how should the interaction between computer algebra systems and dynamic mathematical content on the web be organized?). The talk will discuss these issues and present some of the choices that were made in our design.

Mathematical Formulae Recognition and Logical Structure Analysis of Mathematical Papers

Masakazu Suzuki Kyushu University (Japan)

In most cases the current on-line journals in mathematics are supplied in the form of PDF with print images of papers in the front and OCR'ed hidden texts behind to provide with search facilily using key words. The embedded hidden texts usually does not include good information about mathematical formulae in the papers. We can say that, for the future development of DML, it is desirable to include, in the digitised journals, more structured information of the content of mathematical papers, e.g. tag information to indicate logical structure of papers such as hedding of sections, definitions, theorems, lemmas, etc., together with mathematical formulae structures included.

Against Rigor

Doron Zeilberger (Rutgers University, USA)

The ancient Greeks gave (western) civilization quite a few gifts, but we should beware of Greeks bearing gifts. The gifts of theatre and democracy were definitely good ones, and perhaps even the gift of philosophy, but the "gift" of the so-called "axiomatic method" and the notion of "rigorous" proof did much more harm than good. If we want to maximize Mathematical Knowledge, and its Management, we have to return to Euclid this dubious gift, and give-up our fanatical insistence on perfect rigor. Of course, we should not go to the other extreme, of demanding that everything should be non-rigorous. We should encourage diversity of proof-styles and rigor levels, and remember that nothing is absolutely sure in this world, and there does not exist an absolutely rigorous proof, nor absolute certainty, and "truth" has many shades and levels.