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.4.0.tar.gz
sha512=f957d3d3260b6f2960e59cabb64a1f5636370cee7fc8870911855e331a50e86e2f5ef526f1d27921a15ed4870521346415dd1c0542e8b61c403b9c465eb8cd9e

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:2024-11-15

Published: 15 Nov 2024

Dev Dependencies (2)

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

Conflicts

None