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.0.tar.gz
sha512=7bd5b173ca0dd2d70fd6af03020cc9a8cf05e64e02e6f40a497f8f8d77d456592ad45f12e9ee09db00df641f54e1c00347bdce3e2a6c44547381410e2e27baaa

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-05-26

Published: 26 May 2023

Dependencies (1)

  1. coq-mathcomp-algebra

Dev Dependencies (2)

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

Conflicts

None