

Conferences on Intelligent Computer Mathematics 2010
Paris, France 5th10th July 2010

Invited Speakers

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
mideighties. We try to analyze the reasons of such a slow progress,
pointing out the main problems and suggesting some possible research
directions.
[Springerlink]


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


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"
Although, formally, mathematics is clear that a function is a
singlevalued 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.
In particular we ask whether there might be a constant "de Bruijn factor" as
we make these texts more formal, and conclude that the answer depends greatly on the interpretation being placed on the symbols.
[Springerlink]


The Dynamic Dictionary of Mathematical Functions
Bruno Salvy (INRIA Rocquencourt & MSRInria 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.msrinria.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.
[Springerlink]


Mathematical Formulae Recognition and Logical Structure Analysis of
Mathematical Papers
In most cases the current online 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
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 socalled "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 giveup our fanatical insistence on perfect rigor. Of course, we should
not go to the other extreme, of demanding that everything should be
nonrigorous. We should encourage diversity of proofstyles 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.
[Springerlink]

DML:
AISC:
Calculemus:
MKM:

