Toernooiveld 1
NL-6525 ED Nijmegen
The Netherlands
26th January 2004
Mathematicians produce two things: Theories and documents about the theory. Computers should help them in both activities, but should both activities be covered by the same tool?
I wish to have feedback on my views on how the mathematical document production “work flow” is organised, and what tools should cover what part of the work flow.
Currently, a computer is more useful to a secretary, accountant, etc than to a mathematician. The former trades nowadays routinely use computer programs to help them in their tasks, and most (if not all) their tasks whose computerisation is a win are computerised. For mathematicians, the situation is less optimal: While for some tasks, like in computational algebra, automatisation and computer help is available, effective and widely used, it is my opinion that computers can be much more useful to mathematicians than they are now. One of our goals is to change this, to ensure that, if they wish, mathematicians can make maximal use of computers and get maximal help from computers. For this, we need to understand what mathematicians need, and how the “ideal version” of programs they would use should be organised. This document is a call for opinions on a particular point of this subject.
In the work flow of the mathematician I see two very different activities:
Writing documents about the theory, e.g.
The result of the first is a complete, rigorous presentation of the theory that is read by colleagues. It is to be added to the “big library of all mathematics”. We will thus call it theory library entry. It has very strong requirements of correctness that are, in my opinion, ideally met by fully formalising it, and having the formalisation checked by a De Bruijn criterion compliant theorem checker. It would be “socially acceptable” to require such a theory to be fully formalised before it is generally accepted as valid1; the mathematicians will accept to do this extra step, to spend this extra time (once the tools are mature and this represents an acceptable amount of effort and time). This will save us repeats of e.g. the story of Hilbert's 16th problem (maximal number of limit cycles of a polynomial differential equation in dimension 2) throughout the century, as described in [Ghy01]2. The “reference view” of the mathematical theory presentation can thus, and there are advantages to doing so, be derived more or less automatically from the formalisation.
The second has various audiences (students, colleagues, amateurs, ...). I explicitly make no statement here about the support of the document (cellulose-based paper, interactive or non-interactive electronic document, ...). The requirements of guarantees of total and formal correctness are sometimes/often looser. While a nice extra, I don't see such guarantees becoming a real requirement; (some) mathematicians will refuse to spend the extra time. Weaker forms of checking / formality (like [Ned02] or [Wie]) may be applicable, either as a publication requirement, or as a help to the author to catch typing errors and slips, similarly to automatic spelling and grammar checks done in mainstream document preparation systems. These documents would obviously refer to and incorporate parts of the theory library entry.
The question this note aims to ask is “Do these two different activities warrant two different tools?”. Let's call the tool used for writing library entries LibPerfect and the one used for writing documents about the theory ImpressAudience. It seems natural that LibPerfect would include everything useful to the user when he is building a theory or a result (proof checker, presentation of finished and unfinished proofs to send to colleagues, search facilities to find a lemma proven years earlier, computer algebra system, etc). ImpressAudience would include everything useful to write documents about mathematics (easy use of existing mathematical notations, easy definition of new notations, multiple support (paper, electronic, transparents, ...), etc), ideally not requiring the user to retype what he has already typed in LibPerfect. The question now becomes the question of whether LibPerfect should be distinct from or equal to ImpressAudience.
The equality approach will lead to a very tight integration between the theorem prover and the display engine parts of the system. Temptation will be very big to do a complete system that can work only with one theorem prover, e.g. Coq, as back-end. This will substantially stifle innovation in the theorem prover area, and remove free choice of theorem prover, thus of foundations of mathematics, from the user: People that want to use, e.g. Mizar, will be punished for it because they won't be able to use that magnificent unified tool to write documents, and people using the unified system won't be able to refer to their work. Mizar users will effectively be shunted from the community. This is politically unacceptable: we do not want unique thought to rule us. Science is all about having different people trying different perspectives.
The ideal system, thus, should be a galaxy of inter-operable components, with well-defined and universal interfaces between them. Users will pick their own mix from it: A theorem prover that matches their view of foundations mathematics, a display engine whose input language fits their preferences, ... The question whether this galaxy is possible is open, though. I feel it depends mostly on how much semantics are needed at what point of the chain. The more semantics are needed in a particular stratum, the more this stratum will depend on the exact implementation of the other stratus.
The central, decisive, points seem to be
What's your opinion?