Ένα από τα διασημότερα και δυσκολότερα προβλήματα στην ιστορία των μαθηματικών πέρασε πλέον από τα χέρια των ανθρώπων στους υπολογιστές. Η Anthropic ανακοίνωσε ότι το Claude και μια ομάδα από δεκάδες συνεργαζόμενους AI agents ολοκλήρωσαν μέσα σε μόλις 11 ημέρες την πλήρη επισημοποίηση του τελευταίου θεωρήματος του Φερμά, δημιουργώντας την πρώτη απόδειξη που μπορεί να ελεγχθεί από άκρη σε άκρη από υπολογιστή.
Πρόκειται για μια σημαντική διευκρίνιση: η τεχνητή νοημοσύνη δεν ανακάλυψε μια καινούργια απόδειξη του θεωρήματος. Η απόδειξη είχε ήδη βρεθεί από τον Βρετανό μαθηματικό Άντριου Γουάιλς το 1995. Αυτό που κατάφερε τώρα το Claude ήταν να μετατρέψει την πολύπλοκη μαθηματική λογική της απόδειξης σε κώδικα, έτσι ώστε να μπορεί να ελεγχθεί βήμα προς βήμα από το σύστημα Lean.
Το τελευταίο θεώρημα του Φερμά διατυπώνεται σχετικά απλά: δεν υπάρχουν θετικοί ακέραιοι αριθμοί a, b και c που να ικανοποιούν την εξίσωση aⁿ + bⁿ = cⁿ για οποιονδήποτε ακέραιο n μεγαλύτερο του 2. Ο Πιερ ντε Φερμά είχε γράψει τον 17ο αιώνα ότι είχε ανακαλύψει μια «θαυμάσια απόδειξη», τόσο μεγάλη μάλιστα ώστε δεν χωρούσε στο περιθώριο του βιβλίου του. Για περισσότερους από τρεις αιώνες, όμως, κανείς δεν κατάφερε να την εντοπίσει ή να αποδείξει το θεώρημα.
Ο Γουάιλς παρουσίασε την απόδειξή του το 1993, έπειτα από επτά χρόνια μυστικής εργασίας. Στη συνέχεια εντοπίστηκε ένα σοβαρό κενό στην απόδειξη και χρειάστηκε περίπου ένας ακόμη χρόνος, μαζί με τον μαθηματικό Ρίτσαρντ Τέιλορ, για να διορθωθεί. Η τελική απόδειξη δημοσιεύθηκε το 1995 και εκτεινόταν σε 129 σελίδες.
Ακριβώς εδώ βρίσκεται η σημασία της νέας επιτυχίας της Anthropic. Οι μαθηματικές αποδείξεις είναι δυνατόν να είναι τεράστιες και να βασίζονται σε χιλιάδες επιμέρους βήματα. Ένα λάθος σε ένα μόνο από αυτά μπορεί να θέσει υπό αμφισβήτηση ολόκληρο το αποτέλεσμα. Η «επισημοποίηση» μετατρέπει την απόδειξη σε μια γλώσσα που μπορούν να ελέγξουν οι υπολογιστές, χωρίς να χρειάζεται να βασίζονται στην ανθρώπινη εκτίμηση ότι κάθε βήμα είναι σωστό.
Το μέγεθος του εγχειρήματος είναι εντυπωσιακό. Το Claude δημιούργησε περίπου 13 εκατομμύρια γραμμές κώδικα Lean και απέδειξε περίπου 30.300 θεωρήματα κατά τη διάρκεια της διαδικασίας, από τα οποία περίπου 29.500 χρησιμοποιήθηκαν στην τελική απόδειξη.
Το τελικό αποτέλεσμα είναι πάνω από πέντε φορές μεγαλύτερο από το σύνολο της βιβλιοθήκης Mathlib, της βασικής κοινότητας αποθετηρίου τυποποιημένων μαθηματικών αποδείξεων πάνω στην οποία βασίστηκε η προσπάθεια.
Η προσπάθεια δεν ήταν, πάντως, μια απλή εντολή προς ένα chatbot. Δεκάδες διαφορετικοί AI agents συνεργάστηκαν για να ορίσουν έννοιες, να αποδείξουν ενδιάμεσα θεωρήματα και στη συνέχεια να χρησιμοποιήσουν αυτά τα αποτελέσματα για να προχωρήσουν σε ολοένα δυσκολότερα τμήματα της απόδειξης. Στα πρώτα στάδια, αρκετές προσπάθειες απέτυχαν, καθώς οι agents έχαναν την εικόνα της συνολικής κατάστασης του έργου και σταματούσαν να συνεργάζονται αποτελεσματικά.
Η κατάσταση άλλαξε όταν οι ερευνητές χρησιμοποίησαν το Prove2Me, μια πλατφόρμα σχεδιασμένη για συνεργατική επισημοποίηση μαθηματικών. Το σύστημα διατηρούσε έναν «χάρτη» των εξαρτήσεων μεταξύ των θεωρημάτων και επέτρεπε στους διαφορετικούς agents να γνωρίζουν ποια προβλήματα είχαν ήδη λυθεί και ποιο θα έπρεπε να είναι το επόμενο βήμα τους. Σύμφωνα με την Anthropic, η επιτυχημένη προσπάθεια κατανάλωσε περίπου 6 δισεκατομμύρια output tokens από ένα εσωτερικό ερευνητικό μοντέλο.
Το αποτέλεσμα εξετάστηκε και από τον Κέβιν Μπάζαρντ, μαθηματικό του Imperial College London, ο οποίος είχε ξεκινήσει ένα πολυετές πρόγραμμα για την επισημοποίηση της απόδειξης του Γουάιλς. Ο Μπάζαρντ χαρακτήρισε το επίτευγμα «εξαιρετικό» και τόνισε ότι η αυτόματη επισημοποίηση του τελευταίου θεωρήματος του Φερμά δείχνει πως η τεχνολογία μπορεί πλέον να αποτελέσει ένα σημαντικό βήμα προς την αυτόματη επισημοποίηση μεγάλου μέρους της σύγχρονης μαθηματικής βιβλιογραφίας.
Και αυτό ίσως είναι το πραγματικά σημαντικό κομμάτι της ιστορίας. Η αξία του Claude δεν βρίσκεται μόνο στο ότι κατάφερε να αναπαραστήσει μια ιστορική απόδειξη. Εάν η ίδια διαδικασία μπορεί να εφαρμοστεί σε χιλιάδες άλλες μαθηματικές εργασίες, η τεχνητή νοημοσύνη θα μπορούσε να βοηθήσει τους επιστήμονες να εντοπίζουν λάθη σε πολύπλοκες αποδείξεις, αλλά και να μειώσει δραστικά τον χρόνο που απαιτείται για τον έλεγχο νέων μαθηματικών αποτελεσμάτων.
Η Anthropic υποστηρίζει ότι η συγκεκριμένη απόδειξη χρησιμοποιεί μόνο τα τρία τυπικά αξιώματα του Lean και ότι ο υπολογιστικός έλεγχος επιβεβαίωσε πως η διατύπωση του θεωρήματος αντιστοιχεί σε εκείνη που υπάρχει ήδη στη Mathlib. Με άλλα λόγια, δεν πρόκειται απλώς για ένα ακόμη κείμενο που «μοιάζει» με μαθηματική απόδειξη. Είναι μια απόδειξη που έχει μετατραπεί σε μορφή την οποία ο υπολογιστής μπορεί να ελέγξει μηχανικά.
Για τον Φερμά, χρειάστηκαν περισσότεροι από 350 χρόνια μέχρι να κλείσει οριστικά ο κύκλος. Για τον Γουάιλς χρειάστηκαν επτά χρόνια για να βρει την απόδειξη και ακόμη δύο περίπου χρόνια μέχρι να διορθωθεί και να δημοσιευθεί. Τώρα, η τεχνητή νοημοσύνη χρειάστηκε μόλις 11 ημέρες για να μετατρέψει αυτή την τεράστια μαθηματική κληρονομιά σε μια μορφή που ελέγχεται από μηχανή.
Και ίσως το πιο ενδιαφέρον συμπέρασμα δεν είναι ότι «η AI απέδειξε τον Φερμά», αλλά ότι οι υπολογιστές αρχίζουν πλέον να μπορούν να ελέγχουν σε τεράστια κλίμακα τα ίδια τα θεμέλια των μαθηματικών. Αυτό μπορεί να αλλάξει όχι μόνο τον τρόπο με τον οποίο γράφονται οι αποδείξεις, αλλά και τον τρόπο με τον οποίο οι μαθηματικοί θα τις ελέγχουν στο μέλλον.
Με πληροφορίες από το Newscientist / Anthropic / Secnews
