# Mathematical Components

## About

Welcome to Mathematical Components' web-page!

Mathematical Components are libraries of formalized mathematics developed using the Coq proof assistant. This project finds its roots in the formal proof of the Four Color Theorem. It has been used for large scale formalization projects, including a formal proof of the Odd Order (Feit-Thompson) Theorem.

The libraries are written using the Ssreflect proof language, now part of the standard distribution of the Coq proof assistant.

This is an open source project, licensed under the CeCILL-B free software license agreement.

## Get the library

- Here are installation instructions.
- The current stable release of the Mathematical Components library can be downloaded from github.
- Older versions are available in the historic archive.

## Documentation

- The source file of each library features a documentation header
which describes the concepts and notations introduced in that library.
- 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, as a chapter of Coq's reference manual.
- A book is in progress, and introduces the techniques for writing algorithms and proofs and describing the design ideas of the library.

### More material

- Books, lectures, videos, etc.
- Research papers related to Mathematical Components. Your paper or thesis is not in the list? Send us a message to correct this.

## Help and contact

- Chat with us on gitter!
- Discuss with us on Coq's Discourse forum!
- Subscribe to the Ssreflect mailing list.
- Browse the archives or consult the general information page of the mailing list.

## Authors and contributors

The Mathematical Components library and the Ssreflect proof language were initially developed by the Mathematical Components team at the Inria-Microsoft Research Joint Centre. Today, the list of members of the Mathematical Components organization is visible here.