It (Coq, red.) provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
USE flags for sci-mathematics/coq Proof assistant written in O'Caml
||Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see https://wiki.gentoo.org/wiki/Project:Quality_Assurance/Backtraces|
||Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally|
||Enable support for a graphical user interface|
||Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)|
||Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)|
Coq can be installed from the official gentoo repositories.
emerge --ask sci-mathematics/coq
Users of Visual Studio Code can use the VsCoq extention which is currently maintained by the coq-community.
Users of Vim/Neovim can use the Coqtail plugin.
For a thorough introduction to logic in Coq see the free e-book Logical Foundation from the University of Pennsylvania.