GitHub - tangentforks/FourColorTheorem: Gonthier's formal proof of the 4-color theorem, in Coq.

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 2 Commits
.depend		.depend
LICENSE		LICENSE
Make		Make
Makefile		Makefile
README		README
approx.v		approx.v
birkhoff.v		birkhoff.v
cfcolor.v		cfcolor.v
cfcontract.v		cfcontract.v
cfmap.v		cfmap.v
cfquiz.v		cfquiz.v
cfreducible.v		cfreducible.v
chromogram.v		chromogram.v
color.v		color.v
coloring.v		coloring.v
combinatorial4ct.v		combinatorial4ct.v
configurations.v		configurations.v
connect.v		connect.v
contract.v		contract.v
ctree.v		ctree.v
ctreerestrict.v		ctreerestrict.v
cube.v		cube.v
dataset.v		dataset.v
dedekind.v		dedekind.v
discharge.v		discharge.v
discretize.v		discretize.v
dyck.v		dyck.v
embed.v		embed.v
finitize.v		finitize.v
finset.v		finset.v
fourcolor.v		fourcolor.v
frac.v		frac.v
funs.v		funs.v
geometry.v		geometry.v
grid.v		grid.v
gridmap.v		gridmap.v
gtree.v		gtree.v
gtreerestrict.v		gtreerestrict.v
hubcap.v		hubcap.v
hypermap.v		hypermap.v
initctree.v		initctree.v
initgtree.v		initgtree.v
job001to106.v		job001to106.v
job107to164.v		job107to164.v
job165to189.v		job165to189.v
job190to206.v		job190to206.v
job207to214.v		job207to214.v
job215to218.v		job215to218.v
job219to222.v		job219to222.v
job223to226.v		job223to226.v
job227to230.v		job227to230.v
job231to234.v		job231to234.v
job235to238.v		job235to238.v
job239to253.v		job239to253.v
job254to270.v		job254to270.v
job271to278.v		job271to278.v
job279to282.v		job279to282.v
job283to286.v		job283to286.v
job287to290.v		job287to290.v
job291to294.v		job291to294.v
job295to298.v		job295to298.v
job299to302.v		job299to302.v
job303to306.v		job303to306.v
job307to310.v		job307to310.v
job311to314.v		job311to314.v
job315to318.v		job315to318.v
job319to322.v		job319to322.v
job323to383.v		job323to383.v
job384to398.v		job384to398.v
job399to438.v		job399to438.v
job439to465.v		job439to465.v
job466to485.v		job466to485.v
job486to489.v		job486to489.v
job490to494.v		job490to494.v
job495to498.v		job495to498.v
job499to502.v		job499to502.v
job503to506.v		job503to506.v
job507to510.v		job507to510.v
job511to516.v		job511to516.v
job517to530.v		job517to530.v
job531to534.v		job531to534.v
job535to541.v		job535to541.v
job542to545.v		job542to545.v
job546to549.v		job546to549.v
job550to553.v		job550to553.v
job554to562.v		job554to562.v
job563to588.v		job563to588.v
job589to610.v		job589to610.v
job611to617.v		job611to617.v
job618to622.v		job618to622.v
job623to633.v		job623to633.v
jordan.v		jordan.v
kempe.v		kempe.v
kempetree.v		kempetree.v
matte.v		matte.v
part.v		part.v
patch.v		patch.v
paths.v		paths.v
present.v		present.v
present10.v		present10.v

Repository files navigation

  This directory contains a port to Coq v8 of a fully checked proof of the
Four Colour Theorem, which was originally carried out with version 7.3.1 of
the Coq proof assistant.
  Unlike its predecessor, this formalization requires an extended version of
the Coq v8 system to compile (support for some script-level extensibility
features heavily used by the original proof was discontinued for Coq v8).
  The required extension package, named "ssreflect" (for "small-scale
reflection") is distributed separately. It consists of a single extended ML
(.ml4) file, which compiles to a library that must be linked with the Coq
system, using either the -load-ml-object command line switch (for bytecode
systems, not recommended) or, preferably, the coqmktop utility to produce
a new Coq system binary. The definition of the COQC variable in the Makefile
should be adjusted to refer to this new system (it defaults to ./ssrcoq.exe).
  Note that this directory contains a copy of the vernacular files needed to
support the ssreflect extensions (ssreflect.v and ssrbool.v).