×

Mathematical Components

swMATH ID: 30935
Software Authors: Mathematical Components Team
Description: Mathematical components library: The Mathematical Components Library is an extensive and coherent repository of formalized mathematical theories. It is based on the Coq proof assistant, powered with the Coq/SSReflect language. These formal theories cover a wide spectrum of topics, ranging from the formal theory of general purpose data structures like lists, prime numbers or finite graphs, to advanced topics in algebra. The repository includes the foundation of formal theories used in a formal proof of the Four Colour Theorem (Appel - Haken, 1976) and a mechanization of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory, which utilizes the library extensively.
Homepage: https://math-comp.github.io
Source Code:  https://github.com/math-comp/math-comp
Related Software: Coq; GitHub; Isabelle/HOL; mathlib; hierarchy-builder; PVS; Lean; Nuprl; Mizar; Coquelicot; Isabelle; QuickChick; Nitpick; SmallCheck; QuickCheck; OEIS; FocalTest; Metamath; PCM library; Matita
Cited in: 7 Documents
Further Publications: https://github.com/math-comp/math-comp/wiki/Publications
all top 5

Cited by 12 Authors

2 Affeldt, Reynald
2 Cohen, Cyril
2 Dubois, Catherine
2 Giorgetti, Alain
2 Mahboubi, Assia
2 Sakaguchi, Kazuhiko
1 Chan, Hing-Lun
1 Genestier, Richard
1 Kerjean, Marie
1 Norrish, Michael
1 Rouhling, Damien
1 Sibut-Pinote, Thomas

Cited in 3 Serials

2 Journal of Automated Reasoning
1 Formal Aspects of Computing
1 Logical Methods in Computer Science

Cited in 4 Fields

7 Computer science (68-XX)
2 Number theory (11-XX)
1 Combinatorics (05-XX)
1 Field theory and polynomials (12-XX)

Citations by Year