Le projet math-comp est une bibliothèque de théories mathématiques formalisées, basée sur l'assistant de preuve Coq et le langage Coq/SSReflect. Il couvre un large éventail de sujets, des structures de données de base telles que les listes, les nombres premiers et les graphes fins, à des sujets avancés en algèbre. La bibliothèque a été utilisée dans des preuves formelles de théorèmes importants tels que le théorème des quatre couleurs et le théorème de l'ordre impair.