Δικαιώνεται το λογισμικό που απέδειξε διάσημο μαθηματικό θεώρημα

36

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

Το Θεώρημα των Τεσσάρων Χρωμάτων προτάθηκε από τον μαθηματικό Φράνσις Γκούτιερ το 1852 και υποστηρίζει ότι οποιοσδήποτε γεωγραφικός χάρτης είναι δυνατόν να χρωματιστεί με τέσσερα χρώματα έτσι ώστε καμία περιοχή του χάρτη να μην βρίσκεται σε επαφή με άλλη περιοχή του ίδιου χρώματος.

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

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

Τώρα, ο Τζορτχ Γκόντιερ των εργαστηρίων της Microsoft στη Βρετανία και ο Μπέντζαμιν Ουέρνερ στο INRIA της Γαλλίας υποστηρίζουν ότι απέδειξαν την απόδειξη.

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

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

Ο Γκόντιερ πιστεύει μάλιστα ότι η μελέτη του ίσως προωθήσει περαιτέρω τη χρήση υπολογιστών στα μαθηματικά και αλλάξει τον τρόπο που σκέφτονται οι μαθηματικοί.

Η Microsoft ελπίζει τώρα να αναπτύξει ένα παρόμοιο σύστημα ελέγχου λογικής το οποίο θα σαρώνει τον κώδικα άλλων προγραμμάτων και θα εντοπίζει σφάλματα που κάνουν τον υπολογιστή να κολλάει.

Newsroom ΑΛΤΕΡ ΕΓΚΟ