Four Color Theorem
A formal proof of the Four Color Theorem in Coq, including supporting theories for real numbers, plane topology, and combinatorial hypermaps.
What is Four Color Theorem?
Fourcolor is a Coq library containing a formal proof of the Four Color Theorem, a landmark result in graph theory stating that any planar map can be colored using at most four colors. It provides the complete machine-verified proof along with supporting theories needed to state and prove the theorem, including axiomatization of real numbers and plane topology definitions.
Researchers and practitioners in formal verification, theorem proving, and mathematical logic who need a verified implementation of the Four Color Theorem or foundational theories for real numbers and combinatorial hypermaps.
It offers the only complete, machine-checked formal proof of the Four Color Theorem available in Coq, built on the robust Mathematical Components library with modular installation options for different components.
Overview
Formal proof of the Four Color Theorem [maintainer=@ybertot]
Use Cases
Best For
- Studying formal verification of graph theory theorems
Related Projects
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.
