Η εταιρεία τεχνητής νοημοσύνης Anthropic δημιούργησε μια τυποποιημένη απόδειξη του τελευταίου θεωρήματος του Φερμά. Μια ομάδα AI agents χρειάστηκε μόλις 11 ημέρες για να ολοκληρώσει την εργασία, επιβεβαιώνοντας ότι η απόδειξη που είχε προταθεί από άνθρωπο τη δεκαετία του 1990 είναι σωστή.
Το τελευταίο θεώρημα του Φερμά απασχολούσε τους μαθηματικούς για αιώνες, μέχρι που αποδείχθηκε το 1995 από τον Andrew Wiles. Το θεώρημα λέει ότι δεν υπάρχουν ακέραιοι αριθμοί a, b και c που να ικανοποιούν την εξίσωση aⁿ + bⁿ = cⁿ, όταν το n είναι ακέραιος μεγαλύτερος του 2.
Παρότι διατυπώνεται απλά, η απόδειξή του αποδείχθηκε εξαιρετικά δύσκολη. Ο μαθηματικός Pierre de Fermat έθεσε το πρόβλημα τον 17ο αιώνα και είχε αναφέρει ότι διέθετε μια απόδειξη, την οποία, όπως υποστήριζε, δεν χωρούσε στα περιθώρια του σχολικού βιβλίου που έγραφε.
Τα μαθηματικά περνούν τη μεγαλύτερη αλλαγή στην ιστορία τους.
Πολλοί μαθηματικοί προσπάθησαν και απέτυχαν να βρουν απόδειξη. Ο Wiles δούλεψε στο πρόβλημα για επτά χρόνια μυστικά, πριν ανακοινώσει την ανακάλυψή του το 1993. Οι αποδείξεις συχνά βασίζονται σε εκτενείς λογικούς συλλογισμούς που χτίζονται ο ένας πάνω στον άλλον. Αν ένα μόνο βήμα περιέχει λάθος, ολόκληρη η απόδειξη μπορεί να καταρρεύσει. Αυτό συνέβη και στον Wiles, όταν βρέθηκε σφάλμα στην απόδειξή του, το οποίο χρειάστηκε περίπου έναν χρόνο για να διορθωθεί μαζί με τον συνεργάτη του Richard Taylor.
Η τυποποίηση μαθηματικών θεωρημάτων δίνει λύση σε αυτό το πρόβλημα. Τα βγάζει από το πεδίο του χαρτιού και του μολυβιού και τα μετατρέπει σε μορφή κώδικα, που επιτρέπει στις μηχανές να τα επεξεργάζονται συστηματικά, να ελέγχουν τη λογική τους και να εντοπίζουν τυχόν αδυναμίες. Ήδη υπάρχουν 2 εκατομμύρια γραμμές τυποποιημένων μαθηματικών αποθηκευμένες σε ένα κεντρικό αποθετήριο με την ονομασία Mathlib.
Νωρίτερα φέτος, στο Λονδίνο πραγματοποιήθηκε συνέδριο με ειδικούς της AI, επιστήμονες των υπολογιστών και μαθηματικούς, με πρωτοβουλία του Kevin Buzzard από το Imperial College London, ο οποίος μέχρι την ανακοίνωση της Anthropic εργαζόταν σε ένα πενταετές σχέδιο για την τυποποίηση της απόδειξης των 100 σελίδων των Wiles και Taylor, σε μια γλώσσα προγραμματισμού που ονομάζεται Lean, ώστε να μπορεί να ελεγχθεί επίσημα ως προς την ορθότητά της και να χρησιμοποιηθεί ως βάση για περαιτέρω έρευνα.
Ο Buzzard είχε πει τότε ότι, όταν ξεκίνησε το πρότζεκτ, ήταν βέβαιος για την επιτυχία του, αλλά οι πρόσφατες εξελίξεις στην AI τον είχαν πείσει ότι η ολοκλήρωση θα ερχόταν πολύ πιο γρήγορα απ’ όσο πίστευε αρχικά. Η ανακοίνωση της Anthropic ξεπέρασε πλέον αυτή την προσπάθεια και έδωσε τέλος στο πρόβλημα.
Ο Buzzard δήλωσε σε ανακοίνωση που δημοσίευσε η Anthropic ότι η απόδειξη της εταιρείας δεν αφήνει «καμία υπόθεση πέρα από τα αξιώματα των μαθηματικών». Με απλά λόγια, το ζήτημα έχει λυθεί.
«Στη διαδρομή βλέπουμε αυτοτυποποίηση της άλγεβρας, της αρμονικής ανάλυσης, της γεωμετρίας και της θεωρίας αριθμών, και μαθαίνουμε ότι τα τεχνουργήματα της αυτόματης τυποποίησης από AI είναι πλέον αρκετά στιβαρά ώστε να αποτελούν βάση για περαιτέρω εργασία· η απόδειξη είναι πολυεπίπεδη», είπε ο Buzzard. «Αν η αυτόματη τυποποίηση του FLT είναι πλέον δυνατή, τότε έχουμε κάνει ένα μεγάλο βήμα προς την αυτόματη τυποποίηση της σύγχρονης μαθηματικής βιβλιογραφίας».
Στην ανάρτησή της για την ανακοίνωση, η Anthropic ανέφερε ότι το μοντέλο Claude εργάστηκε συνεχώς και αυτόνομα επί 11 ημέρες για να γράψει την απόδειξη. Συμμετείχαν πολλοί ξεχωριστοί AI agents, στους οποίους ανατέθηκαν διαφορετικά καθήκοντα, όπως η αντιμετώπιση μικρότερων τμημάτων του θεωρήματος.
Ανθρώπινοι ειδικοί έδιναν κατά διαστήματα «οδηγίες υψηλού επιπέδου» για να παραμένει η εργασία σε σωστή πορεία, σύμφωνα με την εταιρεία. Σε αρκετές περιπτώσεις, οι agents «έχασαν την εικόνα της κατάστασης του έργου και σταμάτησαν να συνεργάζονται αποτελεσματικά». Ενδιαφέρον έχει ότι, όπως ανέφερε η εταιρεία, η επιτυχία ήρθε αφότου άρχισε να χρησιμοποιεί ένα εργαλείο σχεδιασμένο για ανθρώπινη μαθηματική συνεργασία, το Prove2Me, το οποίο βοήθησε τους διαφορετικούς agents να παρακολουθούν την εργασία τους και να αποφασίζουν τα επόμενα βήματα.
Η τυποποίηση της Anthropic φτάνει τις 13 εκατομμύρια γραμμές Lean και καλύπτει περίπου 29.500 ενδιάμεσα θεωρήματα που χρειάστηκαν ως σκαλοπάτια για την ολοκλήρωση του συνολικού έργου. Αυτό σημαίνει ότι η απόδειξη είναι πάνω από πέντε φορές μεγαλύτερη από το σύνολο της μέχρι σήμερα δουλειάς στο Mathlib, κάτι που τη φέρνει και ως τη μεγαλύτερη απόδειξη Lean που έχει γραφτεί ποτέ.
Το παρόν κείμενο δημιουργήθηκε με τη χρήση τεχνητής νοημοσύνης.
