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.2.5.tar.gz
sha512=efec54d1ea63cbcb21e1bbdcf0a13631f5a84b2d3bffb52ada1055bcbd3d0778523371abc9756437e7de47d1780d8650271d3570d91b4728094ebba0d3fee291

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:2022-07-13

Published: 23 Oct 2022

Dependencies (3)

  1. coq-mathcomp-algebra
  2. coq-mathcomp-ssreflect >= "1.12" & < "1.20~"
  3. coq >= "8.11" & < "8.20~"

Dev Dependencies

None

Conflicts

None