O Coq é um "provador" de teoremas de maneira interativa. Ele nos auxilia a definir funções, predicados, a verificar as provas e suas consistências de maneira programática. Existem outras ferramentas que tem um propósito similar, como o Isabelle da Universidade de Cambridge, que iremos abordar em outro post.
Para instalar, você pode fazer o download da última release no github ou utilizar o seu gerenciador de pacotes padrão. Outra opção boa é utilizar o docker com a imagem coqorg/coq. Utilize a forma que fique mais adequada a você. Caso tenha alguma dúvida, me avise.
