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)