Top 9 mathcomp open source projects

A proof of Abel-Ruffini theorem.

Finite sets, finite maps, multisets and generic sets

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

Multinomials for the Mathematical Components library.

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

The formal proof of the Odd Order Theorem

Formalization of the basic actuarial mathematics using Coq

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

Stable sort algorithms and their stability proofs in Coq