项目作者: math-comp

项目描述 :
Mathematical Components
高级语言: Coq
项目地址: git://github.com/math-comp/math-comp.git
创建时间: 2015-03-11T13:13:27Z
项目社区:https://github.com/math-comp/math-comp

开源协议:

下载


pipeline status
Join the chat

The Mathematical Components repository

The Mathematical Components Library is an extensive and coherent
repository of formalized mathematical theories. It is based on
the Coq/Rocq proof assistant, powered with the
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 (a fresh or up to date version of opam 2 is required):

  1. opam repo add rocq-released https://rocq-prover.org/opam/released
  2. opam install rocq-mathcomp-boot

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

How to get help

About the stability of the MathComp library

  • The MathComp library has been regularly released since 2008.
    Recently, we have been releasing a new version twice a year,
    in line with the released of the Coq/Rocq proof assistant.
  • Changes are documented systematically in CHANGELOG.md for releases
    and doc/changelog for unreleased changes.
  • We use deprecation warnings to help transitioning to new versions
    (see CONTRIBUTING.md for details about the deprecation policy).

Publications and Tools using MathComp

A collection of papers using the Mathematical Components library