Coq is a formal proof management system, also called an interactive theorem prover. It is used to express mathematical assertions, mechanically check proofs of these assertions, find formal proofs, and extract certified programs.
Downloading the program, installing it, learning it, is explained on Coq's webpage, at https://coq.inria.fr/.
See also:
- Wikipedia article Coq
- Wanted: a “Coq for the working mathematician” on MathOverflow
- Proof Assistants site and the tag coq on that site