目的別で選ぶ定理証明器

1. 俺が書いた証明をチェックしたい　→　Proof Checker　(Mizar)
2. 定理をあたえたら全自動で証明を返してほしい　→　Automatical Theorem Prover　(Djinn, Mathematica)
3. 半自動で証明を手伝ってほしい　→　Proof Assistant　(Coq, Isabell)

ただし、2.は扱える領域が極めて狭いので注意!! そして、証明できないときもある。
1.3.はすべての数学的命題を扱うことができるが、人間の努力も必要である。