ssreflect topic
bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
apery
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
lemma-overloading
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
Abel
A proof of Abel-Ruffini theorem.
algebra-tactics
Ring, field, lra, nra, and psatz tactics for Mathematical Components
finmap
Finite sets, finite maps, multisets and generic sets