COMPUTATION, PROOF, MACHINE Mathematics Enters a (PDF)

COMPUTATION, PROOF, MACHINE Mathematics Enters a New Age Computation is revolutionizing our world, even the inner world of the “pure” mathematician. Mathematical methods – especially the notion of proof – that have their roots in classical antiquity have seen a radical transformation since the 1970s, as successive advances have challenged the priority of reason over computation. Like many revolutions, this one comes from within. Computation, calculation, algorithms – all have played an important role in math- ematical progress from the beginning – but behind the scenes, their contribution obscured in the enduring mathematical literature. To understand the future of mathematics, this fascinating book returns to its past, tracing the hidden history that follows the thread of compu- tation. Along the way it invites us to reconsider the dialogue between mathematics and the natural sciences, as well as the relationship between mathematics and computer science. It also sheds new light on philosophical concepts, such as the notions of analytic and synthetic judgment. Finally, it brings us to the brink of the new age, in which machine intelligence offers new ways of solving mathematical prob- lems previously inaccessible. This book is the 2007 Winner of the Grand Prix de Philosophie de l’Acad´emie Franc¸aise. Mathematician, logician, and computer scientist Gilles Dowek is cur- rently a researcher at the French Institute for Research in Computer Sci- ence and Automation (INRIA). He is a member of the scientific board of the Soci´et´e informatique de France and of CERNA. He has also been a consultant with the National Institute of Aerospace, a NASA-affiliated lab. He is the recipient of the French Mathematical Society’s Grand Prix d’Alembert des Lyc´eens for his popular science work. Pierre Guillot is a lecturer in mathematics at the University of Strasbourg’s Institute of Advanced Mathematical Research (IRMA). Marion Roman is a translator based in France. www.cambridge.org © in this web service Cambridge University Press Cambridge University Press 978-0-521-11801-9 - Computation, Proof, Machine: Mathematics Enters a New Age Gilles Dowek Frontmatter More information  www.cambridge.org © in this web service Cambridge University Press Cambridge University Press 978-0-521-11801-9 - Computation, Proof, Machine: Mathematics Enters a New Age Gilles Dowek Frontmatter More information  Computation, Proof, Machine MATHEMATICS ENTERS A NEW AGE Gilles Dowek French Institute for Research in Computer Science and Automation (INRIA) Translated from the French by Pierre Guillot and Marion Roman www.cambridge.org © in this web service Cambridge University Press Cambridge University Press 978-0-521-11801-9 - Computation, Proof, Machine: Mathematics Enters a New Age Gilles Dowek Frontmatter More information  32 Avenue of the Americas, New York, NY 10013-2473, USA Cambridge University Press is part of the University of Cambridge. It furthers the University’s mission by disseminating knowledge in the pursuit of education, learning, and research at the highest international levels of excellence. www.cambridge.org Information on this title: www.cambridge.org/9780521133777 Original edition: Les M´etamorphoses du calcul © Editions le Pommier – Paris, 2007 English translation © Cambridge University Press 2015 This publication is in copyright. Subject to statutory exception and to the provisions of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. First published as Les M´etamorphoses du calcul 2007 First English edition 2015 Printed in the United States of America A catalog record for this publication is available from the British Library. Library of Congress Cataloging in Publication Data Dowek, Gilles. Computation, proof, machine : mathematics enters a new age / Gilles Dowek, French Institute for Research in Computer Science and Automation (INRIA), Pierre Guillot, Universit´e de Strasbourg, Marion Roman. pages cm Includes bibliographical references and index. ISBN 978-0-521-11801-9 (hardback) – ISBN 978-0-521-13377-7 (pbk.) 1. Mathematics – History – 20th century. 2. Mathematics – History. 3. Mathematics, Ancient. I. Guillot, Pierre, 1978– II. Roman, Marion. III. Title. IV. Title: Mathematics enters a new age. QA26.D69 2015 510.9–dc23 2015004116 ISBN 978-0-521-11801-9 Hardback ISBN 978-0-521-13377-7 Paperback Cambridge University Press has no responsibility for the persistence or accuracy of URLs for external or third-party Internet websites referred to in this publication and does not guarantee that any content on such websites is, or will remain, accurate or appropriate. www.cambridge.org © in this web service Cambridge University Press Cambridge University Press 978-0-521-11801-9 - Computation, Proof, Machine: Mathematics Enters a New Age Gilles Dowek Frontmatter More information  To G´erard Huet www.cambridge.org © in this web service Cambridge University Press Cambridge University Press 978-0-521-11801-9 - Computation, Proof, Machine: Mathematics Enters a New Age Gilles Dowek Frontmatter More information  www.cambridge.org © in this web service Cambridge University Press Cambridge University Press 978-0-521-11801-9 - Computation, Proof, Machine: Mathematics Enters a New Age Gilles Dowek Frontmatter More information  Contents Introduction: In Which Mathematics Sets Out to Conquer New Territories page 1 Part One: Ancient Origins 1 The Prehistory of Mathematics and the Greek Resolution 5 2 Two Thousand Years of Computation 15 Part Two: The Age of Reason 3 Predicate Logic 31 4 From the Decision Problem to Church’s Theorem 44 5 Church’s Thesis 55 6 Lambda Calculus, or an Attempt to Reinstate Computation in the Realm of Mathematics 69 7 Constructivity 73 8 Constructive Proofs and Algorithms 82 Part Three: Crisis of the Axiomatic Method 9 Intuitionistic Type Theory 89 10 Automated Theorem Proving 96 11 Proof Checking 105 12 News from the Field 111 13 Instruments 124 vii www.cambridge.org © in this web service Cambridge University Press Cambridge University Press 978-0-521-11801-9 - Computation, Proof, Machine: Mathematics Enters a New Age Gilles Dowek Frontmatter More information  viii Contents 14 The End of Axioms? 134 Conclusion: As We Near the End of This Mathematical Voyage ... 136 Biographical Landmarks 139 Bibliography 149 www.cambridge.org © in this web service Cambridge University Press Cambridge University Press 978-0-521-11801-9 - Computation, Proof, Machine: Mathematics Enters a New Age Gilles Dowek Frontmatter More information