Το Θεώρημα των Τεσσάρων Χρωμάτων

Πόσα χρώματα χρειάζεστε για να χρωματίσετε έναν χάρτη?

Το 1852 ο μαθηματικός Francis Guthrie υποστήριξε ότι οποιοσδήποτε χάρτης μπορεί να χρωματιστεί μόνο με τέσσερα χρώματα, έτσι ώστε καμία περιοχή του χάρτη να μην "συνορεύει" με άλλη περιοχή του ίδιου χρώματος. Η πρόταση ονομάστηκε το Θεώρημα των Τεσσάρων Χρωμάτων και παρέμεινε αναπόδεικτη για 100 και πλέον χρόνια. Κανένας μαθηματικός δεν μπόρουσε να επιβεβαιώσει το θεώρημα αλλά ούτε να το απορρίψει με κάποιο αντιπαράδειγμα.

Η πρώτη απόδειξη ήρθε το 1976 από τους Αμερικανούς μαθηματικούς Appel και Haken από το Πανεπιστήμιο του Illinois, οι οποίοι χρησιμοποίησαν υπολογιστή για να ελέγξουν χιλιάδες πιθανούς χάρτες.

Η απόδειξη όμως αμφισβητήθηκε, επειδή κανείς δεν μπορεί να διαβάσει και να ελέγξει αυτή την απόδειξη παρά μόνο αν "τρέξει" το συγκεκριμένο πρόγραμμα του υπολογιστή. Επίσης κανένας δεν μπορεί να επιβεβαιώσει ότι στον κώδικα του υπολογιστή δεν υπήρχε κάποιο εγγενές λογικό σφάλμα! Οπότε τι σόι απόδειξη είναι αυτή αν οι μαθηματικοί δεν μπορούν να εκφέρουν γνώμη ως προς την ορθότητα της?

Το 2005 οι Georges Gonthier των εργαστηρίων της Microsoft στη Βρετανία και Benjamin Werner στο INRIA της Γαλλίας υποστήριξαν ότι...απέδειξαν την απόδειξη!

Οι ερευνητές μετέγραψαν την απόδειξη στη γλώσσα υπολογιστή Coq, η οποία χρησιμοποιείται για την αναπαράσταση λογικών προτάσεων και ανέπτυξαν ένα λογισμικό "ελέγχου λογικής", προκειμένου να επιβεβαιώσουν ότι κάθε βήμα που οδηγεί στην απόδειξη είναι σωστό...