Mathematical Components resources

Distribution of the complete formal proof of the Odd Order Theorem

Distribution of the Ssreflect extension and of the Mathematical Components libraries

We are pleased to announce the immediate availability of: 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