package coq-fourcolor

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

Install

Dune Dependency

github.com Edit opam file Versions (9)

Authors

  1. G
    Georges Gonthier

Maintainers

  1. P
    Pierre Roux <pierre.roux@onera.fr>

Sources

v1.2.4.tar.gz
sha512=7b2a54b6d11ed582b72b975a55f36cc992b19cbb59eb69199da13304e2b87cc78bc2699911c5f625190ecff0c07c13cd4c43656e116e0aed8ce595d3f32dd7b0

Description

Proof of the Four Color Theorem

This library contains a formalized proof of the Four Color Theorem, 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

keyword:Four color theorem keyword:small scale reflection keyword:mathematical components logpath:fourcolor

Published: 26 Jan 2022

Dependencies (2)

  1. coq-mathcomp-algebra >= "1.11.0" & < "1.15~"
  2. coq >= "8.11" & < "8.16~"

Dev Dependencies

None

Conflicts

None