package coq-fourcolor

  1. Overview
  2. No Docs
Mechanization of the Four Color Theorem in Coq

Install

Dune Dependency

github.com Edit opam file Versions (9)

Authors

  1. G
    Georges Gonthier

Maintainers

  1. P
    palmskog@gmail.com

Sources

v1.3.1.tar.gz
sha512=ed3f0f70c356339ff0918a45deb32fa6d27f7c66ae224c3c7ff1c3bfd5688761e3aab9f77bb88d5a3ea32ef56a20519f133fd0e46e0f48342557b69c9cc6f3d6

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 date:2023-10-26

Published: 26 Oct 2023

Dependencies (1)

  1. coq-mathcomp-algebra

Dev Dependencies (2)

  1. coq-mathcomp-ssreflect (>= "2.0.0" & < "2.3~") | (= "dev")
  2. coq (>= "8.16" & < "8.21~") | (= "dev")

Conflicts

None