Το 1852 ο μαθηματικός Francis Guthrie υποστήριξε ότι οποιοσδήποτε γεωγραφικός χάρτης μπορεί να χρωματιστεί με τέσσερα χρώματα , έτσι ώστε καμία περιοχή του χάρτη να μην βρίσκεται σε επαφή με άλλη περιοχή του ίδιου χρώματος . Η πρόταση ονομάστηκε το Θεώρημα των Τεσσάρων Χρωμάτων και η πρώτη απόδειξη ήρθε το 1976 από τους Αμερικανούς μαθηματικούς Kenneth Appel and Wolfgang Haken από το Πανεπιστήμιο του Illinois οι οποίοι χρησιμοποίησαν υπολογιστή για να ελέγξουν χιλιάδες πιθανούς χάρτες.
Η απόδειξη όμως αμφισβητήθηκε επειδή κανείς δεν μπορεί να επιβεβαιώσει ότι στον κώδικα του υπολογιστή δεν υπήρχε κάποιο εγγενές λογικό
σφάλμα.
Το 2005 οι Georges Gonthier των εργαστηρίων της Microsoft στη Βρετανία και Benjamin Werner στο INRIA της Γαλλίας υποστηρίζουν ότι απέδειξαν την απόδειξη. Οι ερευνητές μετέγραψαν την απόδειξη στη γλώσσα υπολογιστή Coq, η οποία χρησιμοποιείται για την αναπαράσταση λογικών προτάσεων και ανέπτυξαν ένα λογισμικό ελέγχου λογικής προκειμένου να επιβεβαιώσουν ότι κάθε βήμα που οδηγεί στην απόδειξη είναι σωστό .
Δεν υπάρχουν σχόλια:
Δημοσίευση σχολίου