Formalisation using the proof assistant Coq, the language ssreflect, and the Mathematical Components libraries

Tutorials

• Several winter schools on Mathematical Components have been organised, and their exercises are online. No installation of Coq is needed, as it runs in your browser. Try it, or try and a version for coq users !
• A book has been written !
• A forum , a mailing list, and a stackoverflow tag are also here to discuss. See also the Discourse forum for Coq.

Installing Coq

• On Linux, I would recommend to install Coq with Nix through this method. The page also describe how to install Proof-General, helping you writing Coq with emacs. You can also use coqide, which will be downloaded through coq.
• On Mac you might want to use opam : Coq , Mathcomp
• On Windows, you have an all-included file to download here

Using Mathematical Components Analysis libraries

• You can also try the experimental analysis libraries of the Mathematical Components project. This page describe how to do that.