Σε εκδήλωση στο Λονδίνο, μαθηματικοί σημείωσαν απρόσμενα γρήγορη πρόοδο στην τυποποίηση του τελευταίου θεωρήματος του Φερμά με τη βοήθεια της AI.
Στο λόμπι ενός ξενοδοχείου στο κέντρο του Λονδίνου, οι τουρίστες ετοιμάζονται για μια μέρα περιήγησης μέσα στον καύσωνα. Το προσωπικό, την ίδια ώρα, στρώνει ξανά την τραπεζαρία μετά το πρωινό. Και σε μια αίθουσα συσκέψεων χωρίς παράθυρα, συγκεντρωμένοι ακαδημαϊκοί αναρωτιούνται αν οι άνθρωποι θα έχουν ρόλο στο μέλλον των μαθηματικών, τώρα που η AI μπορεί να αποδεικνύει θεωρήματα μόνη της.
Η γενική αίσθηση στην αίθουσα είναι ένα μείγμα απορίας για το πρόσφατο άλμα στην υπολογιστική νοημοσύνη και ενθουσιασμού για τις δυνατότητες που ανοίγει — μαζί με μια μικρή ανησυχία για το τι σημαίνει αυτό για τους ίδιους προσωπικά.
Μια χρυσή εποχή των μαθηματικών ανατέλλει και οι μαθηματικοί ανησυχούν.
Είκοσι πέντε ερευνητές από διαφορετικά πεδία και χώρες βρίσκονται εδώ για να περάσουν μία εβδομάδα δουλεύοντας στην τυποποίηση του τελευταίου θεωρήματος του Φερμά με προηγμένα μοντέλα AI.
Το τελευταίο θεώρημα του Φερμά απασχολούσε τους μαθηματικούς επί αιώνες, μέχρι να αποδειχθεί το 1993 από τον Andrew Wiles. Λέει ότι δεν υπάρχουν ακέραιοι αριθμοί a, b και c που να ικανοποιούν την εξίσωση aⁿ + bⁿ = cⁿ, όταν το n είναι ακέραιος μεγαλύτερος του 2. Είναι εξαιρετικά εύκολο να διατυπωθεί, αλλά τρομερά δύσκολο να αποδειχθεί.
Τώρα, ο Kevin Buzzard στο Imperial College London εργάζεται σε ένα πενταετές πρόγραμμα για να μετατρέψει τις 100 σελίδες μαθηματικών του Wiles σε κώδικα υπολογιστή με την ονομασία Lean, ώστε να μπορεί να ελεγχθεί τυπικά ως προς την ορθότητά του και να χρησιμοποιηθεί ως βάση για περαιτέρω έρευνα.
Η τυποποίηση μαθηματικών θεωρημάτων τα βγάζει από τον κόσμο του χαρτιού και του μολυβιού και τα τοποθετεί σε μια μορφή που επιτρέπει στους υπολογιστές να τα επεξεργαστούν, ακολουθώντας βήμα βήμα τη λογική και εντοπίζοντας τυχόν λάθη. Ήδη, υπάρχουν 2 εκατομμύρια γραμμές τυποποιημένων μαθηματικών αποθηκευμένες σε ένα κεντρικό αποθετήριο με την ονομασία Mathlib.
Το εργαστήριο έχει φέρει μαζί μαθηματικούς, επιστήμονες υπολογιστών και ειδικούς της AI, με την ελπίδα ότι θα μπορέσουν να προχωρήσουν το σχέδιο του Buzzard ώστε να προστεθεί το τελευταίο θεώρημα του Φερμά σε αυτό το σύνολο, βάζοντας τα πιο πρόσφατα μοντέλα AI να κάνουν μέρος της δύσκολης δουλειάς.
Ομάδες έχουν μαζευτεί γύρω από laptops, με το καθένα να δείχνει ελαφρώς διαφορετικό περιβάλλον για ένα από τα κορυφαία μοντέλα της βιομηχανίας της AI. Η ατμόσφαιρα είναι ζωντανή. Ένα δεύτερο δωμάτιο είχε κλειστεί ώστε όποιος ήθελε να δουλέψει σιωπηλά, αλλά παραμένει άδειο.
Προβλήματα και υποπροβλήματα μοιράζονται, ανατίθενται και λύνονται σταδιακά από ανθρώπινα μυαλά που κατευθύνουν και «σπρώχνουν» την AI. Όπως λέει ο Buzzard, πριν από το εργαστήριο το project είχε συνολικά 20.000 γραμμές κώδικα. Μετά από μόλις την πρώτη μέρα, ο αριθμός αυτός είχε διπλασιαστεί.
Το πρόγραμμα Formalising Fermat χρηματοδοτήθηκε το 2024 και ξεκίνησε αργά, με τον Buzzard να γράφει κώδικα χειροκίνητα, με κόπο. Ο ρυθμός επιταχύνθηκε θεαματικά γύρω στον Δεκέμβριο της περασμένης χρονιάς, λέει ο ίδιος, όταν φάνηκε ότι η ικανότητα των μοντέλων AI να δουλεύουν με προχωρημένα μαθηματικά μεγάλωσε γρήγορα. Έπειτα, τον Μάιο, ένα πρόβλημα 80 ετών που είχε θέσει ο Paul Erdős λύθηκε από μηχανή, αιφνιδιάζοντας πλήρως τον κλάδο. Όλη αυτή η εξέλιξη ανάγκασε τον Buzzard να ξανασκεφτεί το σχέδιό του.
«Πάντα είχα μια ήσυχη σιγουριά ότι θα τα καταφέρναμε. Αλλά τώρα έχουν περάσει δύο χρόνια και η AI έχει γίνει τόσο καλή που το ένστικτό μου είναι πως αυτό είναι γελοίο — αυτό που είπα ότι θα κάνω είναι γελοίο. Ας κάνουμε κάτι δέκα φορές καλύτερο», λέει.
Η απόδειξη του Wiles μπορεί να έφτανε περίπου τις 100 σελίδες, αλλά στηριζόταν σε άλλες περίπου 2.000 σελίδες μαθηματικών από τις δεκαετίες του 1960, του 1970 και του 1980. Το αρχικό σχέδιο του Buzzard ήταν να τυποποιηθεί μόνο η τελική εργασία — ή, τουλάχιστον, οι πιο πρόσφατες βελτιώσεις της — θεωρώντας ότι όλα όσα πατάει είναι σωστά.
Αν όλο το σύνολο των θεωρημάτων ήταν μια πυραμίδα, ο Buzzard είχε σκοπό να ξεκινήσει από το 90% του ύψους της, εκεί όπου βρίσκονται τα πραγματικά ενδιαφέροντα προβλήματα. Τώρα όμως πιστεύει ότι είναι δυνατό να δουλέψει κανείς όλη τη διαδρομή, από την κορυφή μέχρι τη βάση, για λόγους πληρότητας.
Είναι ιδιαίτερα βέβαιος ότι, μέχρι το τέλος του πενταετούς προγράμματός του, θα έχει κάνει αυτό που αρχικά είχε θέσει ως στόχο. Το πόσο θα προχωρήσει από εκεί και πέρα εξαρτάται από το πώς θα εξελιχθεί η AI τα επόμενα χρόνια, από το πόσο κοστίζει η πρόσβαση σε αυτήν και από το πώς θα πάει αυτό το εργαστήριο.
Τα μαθηματικά περνούν τη μεγαλύτερη αλλαγή στην ιστορία τους.
Η Hang Lu Su από το Imperial College London είναι μία από τις ερευνήτριες που συμμετέχουν στο εργαστήριο. Έμαθε μόνη της το Lean πριν από μόλις έξι μήνες, χρησιμοποιώντας το ChatGPT, και τώρα εργάζεται εδώ στην αιχμή της έρευνας.
Οι περισσότεροι μαθηματικοί που γνωρίζει εξακολουθούν να χρησιμοποιούν χαρτί και μολύβι. Άρα η χρήση της AI και η τυποποίηση που βλέπει κανείς εδώ δεν αντιπροσωπεύουν σε καμία περίπτωση το σημερινό πεδίο, όμως εκείνη θεωρεί πως μπορεί να είναι μια εικόνα του μέλλοντός του. «Νιώθω ότι υπάρχει μια βιομηχανοποίηση της πνευματικής διαδικασίας [που συντελείται]», λέει η Su. «Αν μη τι άλλο, τα εργαλεία της AI δουλεύουν τόσο καλά, που είναι κάπως σαν να λέμε: “Εντάξει, ας αφήσουμε [το μοντέλο AI] Claude να δουλέψει, και εμείς τι κάνουμε μετά;”»
Εδώ χρησιμοποιούνται πολλά διαφορετικά εργαλεία, από δωρεάν και ανοιχτού κώδικα μέχρι τα πιο πρόσφατα και ακριβά μοντέλα νεοφυών εταιρειών στις ΗΠΑ. Κανείς στην εκδήλωση δεν μπορεί να πει με ακρίβεια πόσα χρήματα ξοδεύονται σε tokens, τις μονάδες νοημοσύνης της AI με τις οποίες χρεώνεται η πρόσβαση, αλλά οι περισσότεροι συμφωνούν ότι το ποσό θα φτάνει εύκολα σε χιλιάδες λίρες τη μέρα. «Καίω tokens λες και δεν πληρώνω τον λογαριασμό, σίγουρα», λέει η Su.
Για να λυθούν αυτά τα δύσκολα μαθηματικά προβλήματα, η ομάδα θα χρειαστεί ποιότητα αλλά και ποσότητα. Η Su εξηγεί ότι εκείνη και ένας συνάδελφός της προσπαθούσαν να τυποποιήσουν το ίδιο κομμάτι μαθηματικών την πρώτη μέρα του εργαστηρίου. Εκείνη κατέληξε σε μια λύση 800 λέξεων, ενώ ο συνάδελφός της βρήκε μια λύση 400 λέξεων. Και οι δύο θα μπορούσαν να θεωρηθούν ως απόδειξη του συγκεκριμένου θεωρήματος. Όμως η πιο σύντομη εκδοχή, που συντάχθηκε πιο γρήγορα, θα ήταν ευκολότερο να δουλευτεί από την AI στη συνέχεια και επίσης πιο εύκολα κατανοητή από έναν άνθρωπο.
Ο κώδικας που δημιουργείται από την AI μπορεί να είναι φλύαρος, άκομψος και να χρειάζεται πολύ χρόνο για να εκτελεστεί, λέει ο Buzzard. Κάποιες φορές βασίζεται σε χρήση ασαφών λειτουργιών μέσα στο Lean με τρόπους που δεν είναι οι προβλεπόμενοι, και έτσι δεν θα μεταγλωττίζονται σωστά όταν κυκλοφορήσουν ανανεωμένες εκδόσεις.
Πολλοί από τους επιμελητές της βιβλιοθήκης Mathlib είναι επιφυλακτικοί στο να προστεθεί μεγάλος όγκος αυτού του κώδικα Lean που παράγεται από AI, ακόμη κι αν αποδεικνύει θεωρήματα, ακριβώς για αυτόν τον λόγο, λέει ο Buzzard. Σήμερα, ο κώδικας σε αυτή τη βιβλιοθήκη γράφεται από εξειδικευμένους και προσεκτικούς ανθρώπους μαθηματικούς, που φροντίζουν να είναι αποδοτικός, σύντομος και κατανοητός. Αποτελεί σταθερή βάση για μελλοντική δουλειά. Ο κώδικας που παράγεται σε αυτό το εργαστήριο είναι διαφορετικός.
«Φτιάχνουμε ένα στρώμα slop από πάνω — ας το πούμε απλώς slop — και τώρα το ερώτημα είναι: τι γίνεται όταν προσπαθήσουμε να μετακινήσουμε το επόμενο στρώμα; Μπορούμε να χτίσουμε το επόμενο επίπεδο πάνω σε αυτό ή όλα απλώς κολλάνε;» αναρωτιέται ο Buzzard.
Οι εξελίξεις αυτές θέτουν και φιλοσοφικά, υπαρξιακά ερωτήματα για τους μαθηματικούς. Τουλάχιστον, τα εργαλεία που έχουν στη διάθεσή τους αλλάζουν, και μαζί τους θα αλλάξει και η δουλειά τους. Στην πιο τεχνο-αισιόδοξη εκδοχή, όμως, η AI μπορεί κάποια στιγμή να αναλάβει και να επεκτείνει μόνη της τα όρια των γνωστών μαθηματικών, ξεπερνώντας και αντικαθιστώντας την ανθρώπινη σκέψη.
«Όλοι κάνουμε [μαθηματικά] επειδή τα αγαπάμε και επειδή πιστεύουμε ότι έχουν σημασία. Αλλά τώρα έρχεται η AI και ξαφνικά το ερώτημα είναι: στην πραγματικότητα, γιατί το κάνουμε αυτό; Ποιο είναι το νόημα;» λέει ο Buzzard. «Αν μια μηχανή αποδείξει ένα θεώρημα αλλά κανένας άνθρωπος δεν μπορεί να το καταλάβει, τότε τι έχουμε πετύχει;»
Αυτά τα ερωτήματα γίνονται ακόμη πιο αιχμηρά όταν τα μαθηματικά είναι απολύτως αφηρημένα, στο είδος του κόσμου που περιλαμβάνει σφαίρες 38 διαστάσεων ή σύνθετα προβλήματα χωρίς προφανή άμεση εφαρμογή. «Υπάρχει αυτός ο αφηρημένος κόσμος, αλλά υπάρχει άραγε αν δεν υπάρχουν άνθρωποι να τον εκτιμήσουν;» διερωτάται ο Buzzard.
