ComparisonWithOtherSystems

page was renamed from ComparisionWithOtherSystems

There are a number of automatic theorems provers, proof assistants and math formalization systems. Some of them:

• http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html
• http://ghilbert.org
• http://www.qedeq.org/index.html
• http://www.cl.cam.ac.uk/users/jrh/hol-light/
• http://isabelle.in.tum.de/index.html
• http://au.metamath.org/index.html
• http://www.mizar.org
• ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html
• http://www.cs.cornell.edu/Info/Projects/NuPrl/
• http://planetmath.org
• http://www.lemma-one.com/ProofPower/index/

For a more complete list see http://www.cs.ru.nl/~freek/digimath/index.html.

It would be nice to give brief list of their advantages and disadvantages compared to Coq.

=== Why you should choose Coq ===

It's free. Coq is licensed under LGPL, so it's much easier to modify it and develop it. For example, although Mizar has very large theorems collection, there is no prover source available.

It's strict. Comparing Coq to wiki-based systems like http://planetmath.org shows it's that Coq is much nicer organized. Although it's easy to contribute to wiki system, it's hard to manage them. It's hard to trust just wiki.