Mathematical Components

All

27 repositories

math-comp.github.io
Public
https://math-comp.github.io/
HTML
•10•7•2•0•Updated Dec 10, 2025Dec 10, 2025
analysis
Public
Mathematical Components compliant Analysis Library
analysis coq ssreflect mathcomp
Rocq Prover
•
Other
•64•230•89•51•Updated Dec 10, 2025Dec 10, 2025
mczify
Public
Micromega tactics for Mathematical Components
coq proof-automation ssreflect mathcomp rocq rocq-prover
Rocq Prover
•9•28•4•1•Updated Dec 9, 2025Dec 9, 2025
hierarchy-builder
Public
High level commands to declare a hierarchy based on packed classes
coq mathcomp elpi
Rocq Prover
•
MIT License
•25•103•87•23•Updated Dec 9, 2025Dec 9, 2025
math-comp
Public
Mathematical Components
coq ssreflect mathcomp
Rocq Prover
•
Other
•125•660•124•37•Updated Dec 4, 2025Dec 4, 2025
docker-mathcomp
Public
Docker images of coq-mathcomp [maintainer=?]
dockerfile ci docker-image coq opam mathcomp
Dockerfile
•
BSD 3-Clause "New" or "Revised" License
•3•6•3•2•Updated Nov 24, 2025Nov 24, 2025
multinomials
Public
Multinomials for the Mathematical Components library.
coq polynomials ssreflect mathcomp
Rocq Prover
•
Other
•13•16•4•7•Updated Nov 7, 2025Nov 7, 2025
finmap
Public
Finite sets, finite maps, multisets and generic sets
coq ssreflect finite-sets mathcomp
Rocq Prover
•29•51•13•5•Updated Nov 5, 2025Nov 5, 2025
odd-order
Public
The formal proof of the Odd Order Theorem
coq ssreflect mathcomp odd-order-theorem feit-thompson-theorem
Rocq Prover
•16•36•1•2•Updated Nov 5, 2025Nov 5, 2025
real-closed
Public
Theorems for Real Closed Fields
coq ssreflect mathcomp real-closed-fields
Rocq Prover
•12•14•6•2•Updated Nov 4, 2025Nov 4, 2025
Abel
Public
A proof of Abel-Ruffini theorem.
coq ssreflect galois-theory mathcomp abel-ruffini
Rocq Prover
•8•30•1•10•Updated Oct 17, 2025Oct 17, 2025
trajectories
Public
Rocq Prover
•5•0•8•0•Updated Oct 15, 2025Oct 15, 2025
Coq-Combi
Public
Algebraic Combinatorics in Coq
Rocq Prover
•
GNU General Public License v3.0
•8•39•1•1•Updated Oct 8, 2025Oct 8, 2025
mcb
Public
Mathematical Components (the Book)
TeX
•
Other
•26•149•37•1•Updated Oct 7, 2025Oct 7, 2025
algebra-tactics
Public
Ring, field, lra, nra, and psatz tactics for Mathematical Components
coq proof-automation ssreflect mathcomp elpi rocq rocq-prover
Rocq Prover
•4•38•15•0•Updated Sep 15, 2025Sep 15, 2025
cad
Public
Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp
coq ssreflect mathcomp
Rocq Prover
•
GNU Lesser General Public License v3.0
•2•0•0•0•Updated Aug 25, 2025Aug 25, 2025
bigenough
Public
Asymptotic reasoning with bigenough
coq ssreflect mathcomp
Coq
•4•5•0•0•Updated May 9, 2025May 9, 2025
tools
Public
Experimental toolbox to manage PR in mathcomp
Shell
•
MIT License
•2•0•0•1•Updated Apr 8, 2025Apr 8, 2025
dioid
Public
A formalization of the algebraic structure of dioid and associated lemmas (including the Nerode lemma).
coq mathcomp
Coq
•
Other
•2•4•0•0•Updated Feb 27, 2025Feb 27, 2025
math-comp-nix
Public
Nix support for mathcomp packages
Nix
•
GNU General Public License v3.0
•4•3•0•6•Updated Mar 7, 2024Mar 7, 2024
tutorial_material
Public
proof script associated to tutorial material
Coq
•1•17•1•0•Updated Oct 29, 2023Oct 29, 2023
mathcomp-history-before-github
Public archive
The "coqfinitgroup" repository before the switch to github
Coq
•0•3•0•0•Updated Mar 25, 2020Mar 25, 2020
newtonsums
Public
Newton series transformation
coq mathcomp
Coq
•3•1•0•1•Updated Nov 10, 2019Nov 10, 2019
POPLmark
Public
Solutions for the POPLmark challenge
coq ssreflect mathcomp
Coq
•0•8•0•0•Updated Nov 9, 2019Nov 9, 2019
wiki
Public archive
general wiki of the math-comp organization
0•3•0•0•Updated Dec 10, 2018Dec 10, 2018
ssr-manual
Public archive
SSReflect user manual
PostScript
•2•3•2•0•Updated Feb 27, 2018Feb 27, 2018
pnp
Public
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Coq
•19•2•0•0•Updated Dec 22, 2016Dec 22, 2016