# Mathematical Components resources

## Distribution of the complete formal proof of the Odd Order Theorem

- Download
the latest version of the code.
- Explore
the final theory graph (scroll right and down or unzoom, the graph is
big).
- Browse
the progress chart (all the lights are green now).
- Some
figures about version 1.0 of the proof.

## Distribution of the Ssreflect extension and of the Mathematical
Components libraries

We are pleased to announce the immediate availability of:

- the Ssreflect proof language version 1.5 for Coq 8.4 (download the sources, browse the coqdoc)
- the Mathematical Components library version 1.5 for Coq 8.4 (download the sources, browse the coqdoc)

Both are distributed under the

CeCILL
B license (the French equivalent
of the BSD license).

With this release “ssreflect” has been split into
two packages. The Ssreflect one contains the proof language (plugin
for Coq) and a small set of core theory libraries about boolean,
natural numbers, sequences, decidable equality and finite types. The
Mathematical Components one contains advanced theory files covering a
wider spectrum of mathematics.

With respect to version 1.4 the proof
language got a few new features related to forward reasoning and some
bugfixes. The Mathematical Components library features 16 new theory
files and in particular: some field and Galois theory, advanced
character theory and a construction of algebraic numbers.

## User manual of the Ssreflect extension

The

user manual of the Ssreflect extension to the Coq tactic language is published via HAL.
We make our best to update regularily this documentation and to synchronize
this manual with the latest distribution of the Ssreflect extension.

## User discussion list

Comments and bug reports about the Ssreflect tactics and the Mathematical
Components libraries are most welcome on the official mailing list
(

subscribe/unsubsribe ,

archives).

## User contributions

Some extra libraries, extending the content of Mathematical Components, developped by external users:

## Developer's corner

## Looking back in time

- the library
corresponding to ssreflect-1.4
- the library
corresponding to ssreflect-1.3
- the library
corresponding to ssreflect-1.2

## Oldies

- Dowload previous
distributions here
- Coq sources for the proof of the Four Color Theorem,
distributed by Microsoft Research : download