Skip to content

ybertot/math-comp

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

pipeline status Join the chat at https://gitter.im/math-comp/

The Mathematical Components repository

The Mathematical Components Library is an extensive and coherent repository of formalized mathematical theories. It is based on the Coq proof assistant, powered with the Coq/SSReflect language.

These formal theories cover a wide spectrum of topics, ranging from the formal theory of general purpose data structures like lists, prime numbers or finite graphs, to advanced topics in algebra. The repository includes the foundation of formal theories used in a formal proof of the Four Colour Theorem (Appel - Haken, 1976) and a mechanization of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory, which utilizes the library extensively.

Installation

If you already have OPAM installed:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect

Additional packages go by the name of coq-mathcomp-algebra, coq-mathcomp-field, etc... See INSTALL for detailed installation instructions in other scenarios.

How to get help

Publications and Tools using MathComp

A collection of papers using the Mathematical Components library can be found on the wiki.

About

Mathematical Components

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Coq 99.2%
  • Shell 0.2%
  • OCaml 0.2%
  • CSS 0.1%
  • Makefile 0.1%
  • Python 0.1%
  • Other 0.1%