Η Anthropic ανακοίνωσε ότι το Claude ολοκλήρωσε την πρώτη επαληθευμένη από υπολογιστή απόδειξη του Τελευταίου Θεωρήματος του Φερμά

Η Anthropic ανακοίνωσε την Πέμπτη ότι το μοντέλο τεχνητής νοημοσύνης Claude ολοκλήρωσε την πρώτη πλήρη, ελεγμένη από υπολογιστή απόδειξη του Τελευταίου Θεωρήματος του Φερμά, ενός από τα πιο διάσημα αποτελέσματα στα μαθηματικά. Εργαζόμενο σε μεγάλο βαθμό αυτόνομα για 11 ημέρες, το Claude έγραψε την απόδειξη στη γλώσσα προγραμματισμού Lean, παράγοντας 13 εκατομμύρια γραμμές κώδικα και αποδεικνύοντας 29.500 ενδιάμεσα θεωρήματα κατά τη διάρκεια της διαδικασίας.anthropic+1

Ένα σπριντ 11 ημερών μέσα από αιώνες μαθηματικών

Το Τελευταίο Θεώρημα του Φερμά δηλώνει ότι δεν υπάρχουν θετικοί ακέραιοι a, b και c που να ικανοποιούν την εξίσωση aⁿ + bⁿ = cⁿ για οποιονδήποτε ακέραιο n μεγαλύτερο του 2. Διατυπώθηκε για πρώτη φορά από τον Pierre de Fermat γύρω στο 1637 και δεν αποδείχθηκε παρά το 1995, όταν ο Andrew Wiles δημοσίευσε μια απόδειξη 129 σελίδων που χρειάστηκε μήνες ειδικού ελέγχου για να επαληθευτεί.anthropic

Η επισημοποίηση αυτής της απόδειξης, δηλαδή η αναγραφή της με τρόπο ώστε ένας υπολογιστής να μπορεί να ελέγξει κάθε λογικό βήμα, αναμενόταν να διαρκέσει χρόνια. Ο Kevin Buzzard, μαθηματικός στο Imperial College του Λονδίνου, ο οποίος ηγείται μιας ανεξάρτητης προσπάθειας επισημοποίησης του θεωρήματος χρησιμοποιώντας τη Lean, επιβεβαίωσε ότι ο κώδικας μεταγλωττίζεται και είναι σωστός. Σε ανάρτησή του την Παρασκευή, ο Buzzard χαρακτήρισε το επίτευγμα ως μια εξαιρετική επιτυχία αυτόματης επισημοποίησης και σημείωσε ότι η απόδειξη είναι πολυεπίπεδη, καλύπτοντας άλγεβρα, αρμονική ανάλυση, γεωμετρία και θεωρία αριθμών.xenaproject.wordpress+1

Η απόδειξη του Claude ακολουθεί την έκθεση των Darmon, Diamond και Taylor σχετικά με το επιχείρημα των Wiles, Taylor και Wiles, μια απλοποιημένη εκδοχή της αρχικής απόδειξης. Η ανθρώπινη παρέμβαση περιορίστηκε σε περιστασιακές οδηγίες υψηλού επιπέδου από τον ερευνητή της Anthropic, Tianyi Peng, του οποίου η ομάδα στο Πανεπιστήμιο Κολούμπια δημιούργησε την πλατφόρμα Prove2Me που κατέστησε δυνατή την προσπάθεια.anthropic+1

Πώς κατασκευάστηκε η απόδειξη

Αρκετές πρώιμες προσπάθειες απέτυχαν καθώς οι πράκτορες του Claude έχασαν την παρακολούθηση της κατάστασης του έργου και σταμάτησαν να συνεργάζονται αποτελεσματικά. Η σημαντική πρόοδος ήρθε όταν η ομάδα στράφηκε στο Prove2Me, μια ανοιχτή συνεργατική πλατφόρμα που διατηρεί ένα κατευθυνόμενο γράφημα δηλώσεων θεωρημάτων, επιτρέποντας σε πολλούς πράκτορες να εργάζονται παράλληλα και να αποφασίζουν ποιες αποδείξεις θα επιχειρήσουν στη συνέχεια. Χρησιμοποιώντας ένα σύστημα πολλαπλών πρακτόρων βασισμένο στο Claude Code, δεκάδες πράκτορες κατανάλωσαν περίπου έξι δισεκατομμύρια tokens εξόδου από ένα εσωτερικό ερευνητικό μοντέλο που η Anthropic περιγράφει ως συγκρίσιμο με το Claude Fable 5.1.siliconangle+1

Η ολοκληρωμένη απόδειξη επαληθεύτηκε από τη Lean χρησιμοποιώντας μόνο τα τρία βασικά αξιώματά της, ενώ ένας συγκριτής επιβεβαίωσε ότι η διατύπωση του θεωρήματος ταιριάζει με τη διατύπωση του Τελευταίου Θεωρήματος του Φερμά στη βιβλιοθήκη Mathlib. Με 13 εκατομμύρια γραμμές, είναι πάνω από πέντε φορές μεγαλύτερη από τη Mathlib, την κύρια κοινοτική βιβλιοθήκη επισημοποιημένων μαθηματικών.anthropic+1

Τι σημαίνει αυτό για τα μαθηματικά

Ο Buzzard, ο οποίος έλαβε το μήνυμα για το αποτέλεσμα ενώ βρισκόταν σε μουσικό φεστιβάλ και αρχικά θεώρησε τον αποστολέα ως απατεώνα, έγραψε ότι το επίτευγμα σηματοδοτεί μια νέα εποχή: Αν η αυτόματη επισημοποίηση του Τελευταίου Θεωρήματος του Φερμά είναι δυνατή τώρα, τότε έχουμε κάνει ένα μεγάλο βήμα προς την αυτόματη επισημοποίηση της σύγχρονης μαθηματικής βιβλιογραφίας. Σημείωσε ότι τέτοιες τεχνικές θα μπορούσαν να εντοπίσουν σφάλματα στο υπάρχον μαθηματικό σώμα και να ελαφρύνουν το φόρτο εργασίας των κριτών που αξιολογούν νέες εργασίες.anthropic+1

Το ορόσημο αυτό ακολουθεί μια σειρά από εξελίξεις στα μαθηματικά που καθοδηγούνται από την τεχνητή νοημοσύνη. Η Anthropic χρησιμοποίησε το Claude τον περασμένο μήνα για να ανακαλύψει νέες πληροφορίες σχετικά με τη συνάρτηση ζήτα του Riemann, ενώ η ανταγωνίστρια OpenAI χρησιμοποίησε το τελευταίο της μοντέλο για να λύσει αρκετά προβλήματα του Erdős. Η Anthropic χρησιμοποίησε επίσης πρόσφατα το Claude για να καταρρίψει την εικασία του Ιακωβιανού σε τρεις διαστάσεις και άνω. Ο Buzzard, από την πλευρά του, σχολίασε με το χαρακτηριστικό του ύφος: Μου δόθηκε 1 εκατομμύριο λίρες για να τρέξω το έργο μου σε 5 χρόνια, η Anthropic χρειάστηκε μόνο 11 ημέρες, αλλά αναρωτιέμαι αν ξόδεψαν περισσότερα χρήματα.xenaproject.wordpress+2