Το Lean επικυρώνει την απόδειξη του Fermat

Το Lean, το λογισμικό ελέγχου αποδείξεων που χρησιμοποιούν μαθηματικοί σε όλο τον κόσμο, αποδέχθηκε μια πλήρη τυπική διατύπωση του τελευταίου θεωρήματος του Φερμά. Η τυποποίηση δημιουργήθηκε από το σύστημα Claude της Anthropic και δημοσιεύθηκε σε ανοικτό αποθετήριο, χωρίς ανεπίλυτα ενδιάμεσα βήματα, πρόσθετα αξιώματα ή υπολογιστικές παρακάμψεις πέρα από τα συνήθη θεμέλια του Lean (αποθετήριο). Ο Κέβιν Μπά­ζαρντ, μαθηματικός στο Imperial College London, ο οποίος ηγούνταν μιας δικής του προσπάθειας τυποποίησης, μετέγλωττισε ανεξάρτητα το έργο και επιβεβαίωσε ότι περνά τον έλεγχο, χαρακτηρίζοντάς το «εξαιρετικό επίτευγμα αυτόματης τυποποίησης» (Μπά­ζαρντ).

Το μαθηματικό ζήτημα είχε λυθεί προ πολλού: ο Άντριου Γουάιλς απέδειξε το θεώρημα το 1995 και κανένας σοβαρός μαθηματικός δεν αμφισβητούσε το αποτέλεσμα. Εκείνο που παρέμενε ανολοκλήρωτο ήταν η μεταγραφή της απόδειξης σε οδηγίες για έναν απολύτως κυριολεκτικό ελεγκτή, με κάθε ορισμό και κάθε ενδιάμεσο βήμα που ο αρχικός συγγραφέας μπορούσε εύλογα να θεωρήσει αυτονόητο. Σύμφωνα με την Anthropic, δεκάδες πράκτορες τεχνητής νοημοσύνης ολοκλήρωσαν αυτή τη μεταγραφή μέσα σε έντεκα ημέρες τον Αύγουστο, δουλεύοντας παράλληλα μέσω της πλατφόρμας Prove2Me (Anthropic).

Το χρονοδιάγραμμα αυτό, ωστόσο, αφορά μια διαδικασία που δεν μπορούν να αναπαραγάγουν τρίτοι, καθώς το εσωτερικό μοντέλο, η υποδομή συντονισμού, οι αποφάσεις των χειριστών και η υπολογιστική δαπάνη δεν περιλαμβάνονται στη δημόσια έκδοση. Αναπαραγώγιμο είναι το τελικό προϊόν: όποιος διαθέτει επαρκές υπολογιστικό υλικό μπορεί να μεταγλωττίσει εκ νέου το έργο στο Lean και να επιβεβαιώσει ότι η απόδειξη γίνεται δεκτή. Ένας χωριστός ελεγκτής, γραμμένος σε Rust από την Anthropic, εξέτασε το ίδιο τυπικό τεκμήριο και επιβεβαίωσε τη συνέπεια και των 1.052.234 δηλώσεών του (τεχνική έκθεση). Πρόκειται, όμως, για δεύτερη ανάγνωση του ίδιου κειμένου και όχι για ανεξάρτητη ανακατασκευή της ενδεκαήμερης διαδικασίας.

Πώς εργάστηκαν οι πράκτορες

Η τυποποίηση μιας απόδειξης απαιτεί τη μεταγραφή του επιχειρήματος ενός μαθηματικού σε μορφή που επιτρέπει σε ένα πρόγραμμα, χωρίς μαθηματική διαίσθηση, να επαληθεύσει κάθε λογικό βήμα. Η διατύπωση του θεωρήματος είναι παραπλανητικά απλή: για κάθε ακέραιο εκθέτη ίσο ή μεγαλύτερο του τρία, δεν υπάρχουν τρεις θετικοί ακέραιοι που να ικανοποιούν την εξίσωση aⁿ + bⁿ = cⁿ. Η απόδειξη, αντιθέτως, διατρέχει σε εκατοντάδες σελίδες ορισμένα από τα βαθύτερα πεδία της θεωρίας αριθμών.

Το Claude δεν ανακάλυψε νέα μαθηματικά. Τυποποίησε τη γνωστή ακολουθία αποτελεσμάτων που οδηγεί στην απόδειξη του Γουάιλς, ακολουθώντας την παρουσίαση των μαθηματικών Ανρί Νταρμόν, Φρεντ Ντάιαμοντ και Ρίτσαρντ Τέιλορ (Anthropic, τεχνική έκθεση). Η δημιουργική σύλληψη ανήκε στον Γουάιλς και στους προκατόχους του· η συμβολή του Claude ήταν η μεταγραφή της σε περίπου 10,5 εκατομμύρια γραμμές κώδικα, τις οποίες μπορεί να ελέγξει μηχανή (τεχνική έκθεση).

Η πλατφόρμα Prove2Me, την οποία σχεδίασαν ο ερευνητής της Anthropic Τιανγί Πενγκ και συνεργάτες του Columbia University, χώρισε την απόδειξη σε ένα γράφημα εξαρτήσεων με περίπου 29.511 αυτοτελείς ισχυρισμούς (τεχνική έκθεση). Οι πράκτορες επέλεγαν ισχυρισμούς των οποίων οι προϋποθέσεις είχαν ήδη καλυφθεί, έγραφαν τις αποδείξεις στο Lean και έλεγχαν τις προτάσεις άλλων πρακτόρων, ώστε πολλές εργασίες να προχωρούν ταυτόχρονα. Η διαδικασία κατανάλωσε περίπου έξι δισεκατομμύρια διακριτικά εξόδου από ένα εσωτερικό ερευνητικό μοντέλο (τεχνική έκθεση).

Κατά την Anthropic, οι άνθρωποι που επέβλεπαν τη διαδικασία δεν έγραψαν κώδικα Lean, αλλά επέλεξαν το θεώρημα, υπέδειξαν τη γνωστή διαδρομή της απόδειξης, σχεδίασαν την υποδομή των πρακτόρων και κατά διαστήματα άλλαξαν τις προτεραιότητες (Anthropic). Η εταιρεία δεν δημοσιοποίησε ούτε το πλήρες αρχείο των παρεμβάσεων των χειριστών ούτε το υπολογιστικό κόστος.

Στηρίχθηκε σε πολυετή ανθρώπινη εργασία

Το αποτέλεσμα βασίστηκε στο Mathlib, τη μεγάλη βιβλιοθήκη τυποποιημένων μαθηματικών που συντηρεί η κοινότητα, και αξιοποίησε άμεσα δύο προγενέστερα έργα. Η ομάδα του Μπά­ζαρντ στο Imperial κατασκεύαζε από τα τέλη του 2023 μια τυποποίηση του τελευταίου θεωρήματος του Φερμά στο Lean, με χρηματοδότηση 1 εκατ. λιρών από το EPSRC και προγραμματισμένο ορίζοντα έως το 2029 (χρηματοδότηση EPSRC). Ένα χωριστό κοινοτικό έργο είχε ήδη τυποποιήσει το θεώρημα για ένα υποσύνολο περιπτώσεων. Το αρχείο απόδοσης της Anthropic καταγράφει 106 αρχεία με υλικό που αντλήθηκε ή προσαρμόστηκε από αυτές τις προσπάθειες (απόδοση).

Η παράλληλη εκτέλεση καθιστά τις έντεκα ημερολογιακές ημέρες ασύγκριτες με τις ανθρωποώρες που είχε επενδύσει η ομάδα του Μπά­ζαρντ, η οποία εργαζόταν με χρηματοδότηση επί περίπου 22 μήνες όταν άρχισε η προσπάθεια του Claude (χρηματοδότηση EPSRC). Η Anthropic δεν γνωστοποίησε ούτε τις ώρες λειτουργίας των μονάδων επεξεργασίας γραφικών ούτε την ενεργειακή κατανάλωση.

Πριν από αυτή τη δημοσίευση, το τελευταίο θεώρημα του Φερμά ήταν το μοναδικό από τα 100 σημαντικά θεωρήματα στον κατάλογο του Φρέικ Βίνταϊκ που παρέμενε χωρίς τυπική απόδειξη, ένα σημείο αναφοράς μέσω του οποίου καταγράφεται εδώ και δύο δεκαετίες η πρόοδος του κλάδου (Μπά­ζαρντ).

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