Information technology implications for mathematics a view from the French riviera

Information technology implications for mathematics— a view from the French riviera Marco Maggesi and Carlos Simpson Laboratoire J. A. Dieudonne, CNRS UMR 6621 Universite de Nice-Sophia Antipolis . . . la traduction en langage formalise ne serait plus qu'un exercise de patience (sans doutes fort penible). —Nicolas Bourbaki Hanc marginis exiguitas non caperet. —Pierre de Fermat We feel that this context has now changed. For a long time, “mathemat- ics” and “computer science” have designated widely separated disciplines, overlapping only in areas which were considered “fringe” on either side. This was not really a historical view since Von Neumann, Turing and oth- ers were mathematicians who set off into the world of computers. We are now entering a time of reconvergence which has all kinds of implications. A prominent one is the increasing reality of computer proof verification as applied to standard mathematical work. This has been under development for quite a while, but just now it is becoming realistic to imagine applying it to a wide array of mathematical situations. The idea is to write mathematical documents in a language such that the mathematical accuracy is then verified by a computer program. This should be compared with other different but related utilisations of the computer: —typesetting: we are looking at having the computer understand the argu- ment, not just the visual expression on the page, nevertheless on a sociolog- ical level there are many similarities with the TEXproject; —computer algebra and other calculation systems: we are looking at the logical or “proof” aspect of mathematics,effort can higher-order than can stimulate order logic proprietary system his mathematical background trivial theorem apparently has latent theorem-verification possibilities