package coq-fourcolor
Mechanization of the Four Color Theorem in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.4.1.tar.gz
sha512=0efc2465fb34bc7013114e835a58efc3649b84924af72dde5e15084532c48f1b17d0582c48f3cf42eec1dc26ca05df7d53958a65fc9b80fa4bfae9e45907397c
Description
This library contains a formal proof of the Four Color Theorem in Coq, along with the theories needed to support stating and then proving the Theorem. This includes an axiomatization of the setoid of classical real numbers, basic plane topology definitions, and a theory of combinatorial hypermaps.
Tags
category:Mathematics/Combinatorics and Graph Theory keyword:Four color theorem keyword:small scale reflection keyword:Mathematical Components logpath:fourcolor.proof date:2025-04-16Published: 21 Apr 2025
Dependencies (2)
-
coq-fourcolor-reals
= version - coq-mathcomp-algebra
Dev Dependencies (2)
-
coq-mathcomp-ssreflect
(>= "2.1.0" & < "2.5~") | (= "dev") -
coq
(>= "8.18" & < "9.1~") | (= "dev")
Used by (1)
Conflicts
None
On This Page