The Four Colour Theorem: Engineering of a Formal Proof
From MaRDI portal
Publication:3598006
DOI10.1007/978-3-540-87827-8_28zbMATH Open1166.68346OpenAlexW1503170941MaRDI QIDQ3598006FDOQ3598006
Authors: Georges Gonthier 
Publication date: 29 January 2009
Published in: Computer Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-87827-8_28
Recommendations
- Formal proof - the four color theorem
- scientific article; zbMATH DE number 1021588
- The four-colour theorem
- The complexity of the four colour theorem
- scientific article; zbMATH DE number 1564003
- A note on the four color theorem
- An approximate restatement of the Four-Color Theorem
- scientific article; zbMATH DE number 849955
Cited In (35)
- Towards Formal Proof Script Refactoring
- A proof system for graph (non)-isomorphism verification
- Formalization \textit{of} quantum protocols using Coq
- Tests and proofs for custom data generators
- Proof checking and logic programming
- Proof checking and logic programming
- Formalising Mathematics in Simple Type Theory
- A fully automatic theorem prover with human-style output
- Incorporating quotation and evaluation into Church's type theory
- On planarity of graphs in homotopy type theory
- The Jordan Curve Theorem, Formally and Informally
- Applications of real number theorem proving in PVS
- Formalising the double-pushout approach to graph transformation
- Formal proof - the four color theorem
- Pure Pointer Programs with Iteration
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Pollack-inconsistency
- Automated mathematical discovery and verification: minimizing pentagons in the plane
- How hard is positive quantification?
- Computational logic: its origins and applications
- Constructive Mathematics and Functional Programming (Abstract)
- A Compiled Implementation of Normalization by Evaluation
- Formalizing physics: automation, presentation and foundation issues
- The complexity of the four colour theorem
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
- Working with Mathematical Structures in Type Theory
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
- Proof auditing formalised mathematics
- Hammer for Coq: automation for dependent type theory
- What is the point of computers? A question for pure mathematicians
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- Tests and Proofs for Enumerative Combinatorics
- Title not available (Why is that?)
- Proof-producing reflection for HOL. With an application to model polymorphism
Uses Software
This page was built for publication: The Four Colour Theorem: Engineering of a Formal Proof
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3598006)
