The Seventeen Provers of the World

This page is the home of a comparison between proof assistants by having a proof of the irrationality of the square root of two in seventeen different proof assistants. There is also something like a consumer test of these systems.

Here are the source files of those proofs:

  1. HOL Light by John Harrison: hol.ml hol_alt.ml; HOL4 by Konrad Slindt: hol4.ml; ProofPower by Rob Arthan: proofpower.ml
  2. Mizar by Andrzej Trybulec: mizar.miz
  3. PVS by Bart Jacobs and John Rushby: pvs.dmp
  4. Coq by Laurent Théry: coq.v coq_letouzey.v coq_gonthier.v; Matita by Andrea Asperti: matita.ma
  5. Otter/Ivy by Michael Beeson and William McCune: otter.in otter.out ivy.in ivy.out
  6. Isabelle/Isar by Markus Wenzel: isar.thy; script style by Larry Paulson: isabelle.thy; Isabelle/ZF by Larry Paulson: isabelle_ZF.thy
  7. Alfa/Agda by Thierry Coquand: agda.alfa
  8. ACL2 by David Russinoff: acl2.lisp acl2.out; ACL2(r) by Ruben Gamboa: acl2r.event acl2r.out
  9. PhoX by Christophe Raffalli and Paul Rozière: phox.phx
  10. IMPS by William Farmer: imps.t
  11. Metamath by Norman Megill: metamath.mm
  12. Theorema by Wolfgang Windsteiger, Bruno Buchberger, Markus Rosenkranz: theorema.nb theorema_notRatSqrt2.nb theorema_coprime.nb
  13. Lego by Conor McBride: lego.l
  14. Nuprl by Paul Jackson: nuprl.thy nuprl.prl
  15. Omega, by Christoph Benzmüller, Armin Fiedler, Andreas Meier and Martin Pollet: omega.rpy omega.pds
  16. B method, by Dominique Cansell: b.mch b.arc
  17. Minlog, by Helmut Schwichtenberg: minlog.scm minlog_unary.scm

Some of these files are now a few years old: they might not work with the latest version of the corresponding system.

(last modification 2007-02-27)