Coq is a formal proof management system, for formalizing and machine-checking proof written in Ocaml. Coq is based on the Calculus of Inductive Constructions. From the official website
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|
||Add support for x11-libs/gtk+ (The GIMP Toolkit)|
||Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)|
Coq can be installed from the official gentoo repositories.
emerge --ask sci-mathematics/coq
Coq supports multiple user interfaces, such as VSCode, Emacs, Vim/Neovim as well as its own CoqIDE.
Users of Visual Studio Code can use the VsCoq extention which is currently maintained by the coq-community.
Users of Emacs can use the major Coq mode Proof General and extend that with the minor Coq mode Company-Coq.
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.