Repositories list

• analysis

  Public
  Mathematical Components compliant Analysis Library

  analysiscoqssreflect+ 2

  analysiscoqssreflectmathcomprocq

  Rocq Prover

  •

  Other

  •6565 forks•241241 stars•9494 issues•6060 pull requests•Updated Apr 19, 2026Apr 19, 2026

• math-comp

  Public

  math-comp/math-comp’s past year of commit activity
  Mathematical Components

  coqcoq-formalizationssreflect+ 5

  coqcoq-formalizationssreflectmathcomprocqrocq-proverrocq-libraryrocq-prover-lang

  Rocq Prover

  •

  Other

  •129129 forks•677677 stars•134134 issues•3636 pull requests•Updated Apr 17, 2026Apr 17, 2026

• odd-order

  Public
  The formal proof of the Odd Order Theorem

  coqssreflectmathcomp+ 2

  coqssreflectmathcompodd-order-theoremfeit-thompson-theorem

  Rocq Prover

  •1616 forks•3737 stars•11 issue•22 pull requests•Updated Apr 17, 2026Apr 17, 2026

• hierarchy-builder

  Public
  High level commands to declare a hierarchy based on packed classes

  coqmathcompelpi

  coqmathcompelpi

  Rocq Prover

  •

  MIT License

  •3030 forks•104104 stars•9494 issues•2727 pull requests•Updated Apr 15, 2026Apr 15, 2026

• multinomials

  Public

  math-comp/multinomials’s past year of commit activity
  Multinomials for the Mathematical Components library.

  coqpolynomialsssreflect+ 1

  coqpolynomialsssreflectmathcomp

  Rocq Prover

  •

  Other

  •1313 forks•1717 stars•44 issues•66 pull requests•Updated Apr 14, 2026Apr 14, 2026

• algebra-tactics

  Public
  Ring, field, lra, nra, and psatz tactics for Mathematical Components

  coqproof-automationssreflect+ 4

  coqproof-automationssreflectmathcompelpirocqrocq-prover

  Rocq Prover

  •44 forks•3838 stars•1414 issues•11 pull request•Updated Apr 3, 2026Apr 3, 2026

• finmap

  Public
  Finite sets, finite maps, multisets and generic sets

  coqssreflectfinite-sets+ 1

  coqssreflectfinite-setsmathcomp

  Rocq Prover

  •2929 forks•5151 stars•1212 issues•44 pull requests•Updated Apr 1, 2026Apr 1, 2026

• bigenough

  Public
  Asymptotic reasoning with bigenough

  coqssreflectmathcomp

  coqssreflectmathcomp

  Rocq Prover

  •55 forks•55 stars•00 issues•00 pull requests•Updated Mar 26, 2026Mar 26, 2026

• real-closed

  Public
  Theorems for Real Closed Fields

  coqssreflectmathcomp+ 1

  coqssreflectmathcompreal-closed-fields

  Rocq Prover

  •1212 forks•1414 stars•66 issues•11 pull request•Updated Mar 26, 2026Mar 26, 2026

• mczify

  Public

  math-comp/mczify’s past year of commit activity
  Micromega tactics for Mathematical Components

  coqproof-automationssreflect+ 3

  coqproof-automationssreflectmathcomprocqrocq-prover

  Rocq Prover

  •99 forks•2828 stars•44 issues•11 pull request•Updated Mar 25, 2026Mar 25, 2026

• trajectories

  Public
  Rocq Prover

  •55 forks•00 stars•88 issues•00 pull requests•Updated Mar 15, 2026Mar 15, 2026

• Abel

  Public
  A proof of Abel-Ruffini theorem.

  coqssreflectgalois-theory+ 2

  coqssreflectgalois-theorymathcompabel-ruffini

  Rocq Prover

  •99 forks•3030 stars•11 issue•1010 pull requests•Updated Mar 6, 2026Mar 6, 2026

• docker-mathcomp

  Public
  Docker images of coq-mathcomp [maintainer=?]

  dockerfilecidocker-image+ 3

  dockerfilecidocker-imagecoqopammathcomp

  Dockerfile

  •

  BSD 3-Clause "New" or "Revised" License

  •33 forks•66 stars•33 issues•11 pull request•Updated Feb 26, 2026Feb 26, 2026

• math-comp.github.io

  Public
  https://math-comp.github.io/

  HTML

  •1111 forks•77 stars•22 issues•00 pull requests•Updated Feb 18, 2026Feb 18, 2026

• Coq-Combi

  Public
  Algebraic Combinatorics in Coq

  Rocq Prover

  •

  GNU General Public License v3.0

  •88 forks•3838 stars•11 issue•11 pull request•Updated Jan 25, 2026Jan 25, 2026

• mcb

  Public
  Mathematical Components (the Book)

  TeX

  •

  Other

  •2727 forks•151151 stars•3737 issues•22 pull requests•Updated Oct 7, 2025Oct 7, 2025

• cad

  Public
  Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp

  coqssreflectmathcomp

  coqssreflectmathcomp

  Rocq Prover

  •

  GNU Lesser General Public License v3.0

  •22 forks•00 stars•00 issues•00 pull requests•Updated Aug 25, 2025Aug 25, 2025

• tools

  Public
  Experimental toolbox to manage PR in mathcomp

  Shell

  •

  MIT License

  •22 forks•00 stars•00 issues•11 pull request•Updated Apr 8, 2025Apr 8, 2025

• dioid

  Public
  A formalization of the algebraic structure of dioid and associated lemmas (including the Nerode lemma).

  coqmathcomp

  coqmathcomp

  Coq

  •

  Other

  •22 forks•44 stars•00 issues•00 pull requests•Updated Feb 27, 2025Feb 27, 2025

• math-comp-nix

  Public
  Nix support for mathcomp packages

  Nix

  •

  GNU General Public License v3.0

  •44 forks•33 stars•00 issues•66 pull requests•Updated Mar 7, 2024Mar 7, 2024

• tutorial_material

  Public
  proof script associated to tutorial material

  Coq

  •11 fork•1717 stars•11 issue•00 pull requests•Updated Oct 29, 2023Oct 29, 2023

• mathcomp-history-before-github

  Public archive
  The "coqfinitgroup" repository before the switch to github

  Coq

  •00 forks•33 stars•00 issues•00 pull requests•Updated Mar 25, 2020Mar 25, 2020

• newtonsums

  Public
  Newton series transformation

  coqmathcomp

  coqmathcomp

  Coq

  •33 forks•11 star•00 issues•11 pull request•Updated Nov 10, 2019Nov 10, 2019

• POPLmark

  Public
  Solutions for the POPLmark challenge

  coqssreflectmathcomp

  coqssreflectmathcomp

  Coq

  •00 forks•88 stars•00 issues•00 pull requests•Updated Nov 9, 2019Nov 9, 2019

• wiki

  Public archive
  general wiki of the math-comp organization

  00 forks•33 stars•00 issues•00 pull requests•Updated Dec 10, 2018Dec 10, 2018

• ssr-manual

  Public archive
  SSReflect user manual

  PostScript

  •22 forks•33 stars•22 issues•00 pull requests•Updated Feb 27, 2018Feb 27, 2018

• pnp

  Public
  Lecture notes for a short course on proving/programming in Coq via SSReflect.

  Coq

  •1919 forks•22 stars•00 issues•00 pull requests•Updated Dec 22, 2016Dec 22, 2016