###
About

The Mathematical Components library for
Coq has its origins in
the formal proof of the Four Colour Theorem. Since then it has grown
to cover many areas of mathematics and has been used for
large scale projects like the formal proof of the Odd Order Theorem.

The library is written using the Ssreflect proof language that is an integral
part of the distribution.

###
Getting the library

The current stable release of the
Mathematical Components library can be
downloaded from github.

Older versions of the library are available
in the historic archive.

###
Documentation

Each source files features a documentation header which
describes the concepts and notations introduced in that file.
The coqdoc presentation of the source files can be browsed online.

The library graph can be browsed interactively.

The Ssreflect language comes with a dedicated
reference manual.

We also wrote a book introducing the techniques for writing
algorithms and proofs and describing the design ideas of the library.

###
Contact

Interested?
Subscribe to the ssreflect mailing list
and let us know what you are using our libraries for, ask questions, etc.
You can also browse the archives of the list or consult the
general information page.

###
Authors and Contributors

The Mathematical Components library and the Ssreflect proof language
are developed by the
Mathematical Components team, at the
Inria -- Microsoft Research Joint Centre.