詳しい説明は Wikipedia や 本家 (英語) に譲って簡単に説明すると、 Coq とは 正しい事を機械的に確認できる証明 を人間が書く手助けをするシステムです。
四色定理 や Feit-Thompson theorem など 人間では困難な証明の確認を機械的に実行するのに用いられているようです。
ここでは Coq の基本的な使い方をごく簡単に紹介します。
より詳しい情報については以下を参照してください。
Debian, Ubuntu などの場合は、端末から
$ sudo apt-get install coq libssreflect-coqを実行します。
Windows, OS X に関しては こちらの記事 が参考になると思います。