The Seventeen Provers of the World

Foreword by Dana S. Scott

  • Freek Wiedijk

Part of the Lecture Notes in Computer Science book series (LNCS, volume 3600)

Also part of the Lecture Notes in Artificial Intelligence book sub series (LNAI, volume 3600)

Table of contents

  1. Front Matter
  2. Freek Wiedijk
    Pages 1-9
  3. Henk Barendregt
    Pages 10-10
  4. HOL
    John Harrison, Konrad Slind, Rob Arthan
    Pages 11-19
  5. Andrzej Trybulec
    Pages 20-23
  6. PVS
    Bart Jacobs, John Rushby
    Pages 24-27
  7. Coq
    Laurent Théry, Pierre Letouzey, Georges Gonthier
    Pages 28-35
  8. Michael Beeson, William McCune
    Pages 36-40
  9. Markus Wenzel, Larry Paulson
    Pages 41-49
  10. Thierry Coquand
    Pages 50-54
  11. Ruben Gamboa
    Pages 55-66
  12. Christophe Raffalli, Paul Rozière
    Pages 67-71
  13. William Farmer
    Pages 72-87
  14. Norman Megill
    Pages 88-95
  15. Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz
    Pages 96-107
  16. Conor McBride
    Pages 108-115
  17. Paul Jackson
    Pages 116-126
  18. Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet, Jörg Siekmann
    Pages 127-141
  19. Dominique Cansell
    Pages 142-150
  20. Helmut Schwichtenberg
    Pages 151-157
  21. Back Matter

About this book


Commemorating the 50th anniversary of the first time a mathematical theorem was proven by a computer system, Freek Wiedijk initiated the present book in 2004 by inviting formalizations of a proof of the irrationality of the square root of two from scientists using various theorem proving systems.

The 17 systems included in this volume are among the most relevant ones for the formalization of mathematics. The systems are showcased by presentation of the formalized proof and a description in the form of answers to a standard questionnaire. The 17 systems presented are HOL, Mizar, PVS, Coq, Otter/Ivy, Isabelle/Isar, Alfa/Agda, ACL2, PhoX, IMPS, Metamath, Theorema, Leog, Nuprl, Omega, B method, and Minlog.


Coq Isabelle computer algebra systems formal methods formal reasoning systems formal verification formalization mathematical formalizations mathematical proof assistants mathematics provers proving theorem proving theorem proving systems

Editors and affiliations

  • Freek Wiedijk
    • 1
  1. 1.Institute for Computing and Information SciencesRadboud University NijmegenNijmegenThe Netherlands

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2006
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Computer Science Computer Science (R0)
  • Print ISBN 978-3-540-30704-4
  • Online ISBN 978-3-540-32888-9
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site