Στο λόμπι ενός ξενοδοχείου στο κέντρο του Λονδίνου, τουρίστες προετοιμάζονται για μια μέρα περιήγησης μέσα στον καύσωνα. Την ίδια ώρα, το προσωπικό στρώνει ξανά την τραπεζαρία μετά το πρωινό. Και σε μια αίθουσα συσκέψεων χωρίς παράθυρα, συγκεντρωμένοι ακαδημαϊκοί αναρωτιούνται αν οι άνθρωποι θα έχουν ρόλο στο μέλλον των μαθηματικών, από τη στιγμή που η τεχνητή νοημοσύνη μπορεί πια να αποδεικνύει θεωρήματα μόνη της.
Η γενική αίσθηση στην αίθουσα είναι ένα μείγμα απορίας για το πρόσφατο άλμα της υπολογιστικής νοημοσύνης, ενθουσιασμού για όσα ανοίγει αυτό το άλμα και, ίσως, μιας ελαφριάς ανησυχίας για το τι σημαίνει προσωπικά για τους ίδιους το μέλλον.
Μια χρυσή εποχή των μαθηματικών ανατέλλει και οι μαθηματικοί πανικοβάλλονται
Είκοσι πέντε ερευνητές από διαφορετικά πεδία και χώρες βρίσκονται εκεί για να περάσουν μία εβδομάδα δουλεύοντας πάνω στην τυπική μορφοποίηση του τελευταίου θεωρήματος του Φερμά με αιχμής μοντέλα τεχνητής νοημοσύνης.
Το τελευταίο θεώρημα του Φερμά προβλημάτιζε τους μαθηματικούς επί αιώνες, μέχρι που αποδείχθηκε το 1993 από τον Andrew Wiles. Λέει ότι δεν υπάρχουν ακέραιοι αριθμοί a, b και c που να ικανοποιούν την εξίσωση aⁿ + bⁿ = cⁿ, όταν το n είναι ακέραιος μεγαλύτερος του 2. Είναι εξαιρετικά εύκολο να διατυπωθεί, αλλά εξαιρετικά δύσκολο να αποδειχθεί.
Τώρα, ο Kevin Buzzard στο Imperial College London εργάζεται σε ένα πενταετές πρόγραμμα για να μετατρέψει τις 100 σελίδες μαθηματικών του Wiles σε κώδικα υπολογιστή που ονομάζεται Lean, ώστε να μπορεί να ελεγχθεί τυπικά για την ορθότητά του και να αποτελέσει βάση για περαιτέρω έρευνα.
Η τυπική μορφοποίηση μαθηματικών θεωρημάτων τα βγάζει από τον χώρο του χαρτιού και του μολυβιού και τα τοποθετεί σε ένα περιβάλλον που επιτρέπει στους υπολογιστές να τα επεξεργαστούν, να ακολουθήσουν μεθοδικά τη λογική τους και να εντοπίσουν τυχόν λάθη. Ήδη, σε ένα κεντρικό αποθετήριο με το όνομα Mathlib υπάρχουν 2 εκατομμύρια γραμμές τυποποιημένων μαθηματικών.
Αυτό το εργαστήριο έφερε μαζί μαθηματικούς, επιστήμονες υπολογιστών και ειδικούς στην τεχνητή νοημοσύνη, με την ελπίδα ότι θα μπορέσουν να προωθήσουν το σχέδιο του Buzzard να προστεθεί το τελευταίο θεώρημα του Φερμά σε αυτό το σώμα γνώσης, βάζοντας τα πιο πρόσφατα μοντέλα AI να σηκώσουν το μεγαλύτερο βάρος της δουλειάς.
Ομάδες έχουν μαζευτεί γύρω από φορητούς υπολογιστές, με οθόνες που δείχνουν λίγο διαφορετικά περιβάλλοντα για ένα από τα κορυφαία μοντέλα της βιομηχανίας AI. Η ατμόσφαιρα είναι ζωηρή. Έχει κλειστεί και δεύτερη αίθουσα, ώστε όποιος θέλει να δουλέψει ήσυχα να μπορεί να το κάνει, αλλά παραμένει άδεια.
Προβλήματα και υποπροβλήματα μοιράζονται, κατανέμονται και λύνονται σταδιακά από ανθρώπινα μυαλά που καθοδηγούν και κατευθύνουν την AI. Πριν από το εργαστήριο υπήρχαν συνολικά 20.000 γραμμές κώδικα στο πρότζεκτ, λέει ο Buzzard. Μετά από μόλις την πρώτη ημέρα, είχαν διπλασιαστεί.
Το πρότζεκτ Formalising Fermat χρηματοδοτήθηκε το 2024 και ξεκίνησε αργά, καθώς ο Buzzard έγραφε με το χέρι κώδικα με μεγάλη δυσκολία. Ο ρυθμός επιταχύνθηκε θεαματικά γύρω στον Δεκέμβριο του περασμένου έτους, λέει, όταν η ισχύς των μοντέλων AI να δουλεύουν με προχωρημένα μαθηματικά φάνηκε να αυξάνεται γρήγορα. Έπειτα, τον Μάιο, ένα πρόβλημα 80 ετών που είχε θέσει ο Paul Erdős λύθηκε από μηχανή, αιφνιδιάζοντας πλήρως το πεδίο. Όλη αυτή η εξέλιξη τον έκανε να ξανασκεφτεί το σχέδιό του.
«Πάντα ήμουν ήσυχα βέβαιος ότι θα πετύχουμε. Αλλά τώρα είμαστε δύο χρόνια μέσα και η AI έχει γίνει τόσο καλή, που το ένστικτό μου είναι πως αυτό είναι γελοίο – αυτό που είπα ότι θα κάνω είναι γελοίο. Ας κάνουμε κάτι δέκα φορές καλύτερο», λέει.
Η απόδειξη του Wiles μπορεί να έφτανε περίπου τις 100 σελίδες, αλλά στηριζόταν σε άλλες 2.000 περίπου σελίδες μαθηματικών από τις δεκαετίες του 1960, του 1970 και του 1980. Το αρχικό σχέδιο του Buzzard ήταν να τυποποιήσει μόνο την τελική εργασία –ή τουλάχιστον πιο πρόσφατες βελτιώσεις της– υποθέτοντας όμως ότι όλα όσα στηρίζονταν πάνω της ήταν σωστά.
Αν το σύνολο των θεωρημάτων ήταν μια πυραμίδα, ο Buzzard σκόπευε να ξεκινήσει την αναρρίχηση από το 90% της διαδρομής προς την κορυφή, εκεί όπου βρίσκονται τα πραγματικά ενδιαφέροντα προβλήματα. Τώρα όμως πιστεύει ότι είναι δυνατό να αντιμετωπιστεί ολόκληρη η δομή από πάνω μέχρι κάτω, χάριν πληρότητας.
Είναι απολύτως βέβαιος ότι, μέχρι το τέλος του πενταετούς προγράμματός του, θα έχει κάνει αυτό που αρχικά είχε βάλει στόχο. Το πόσο θα προχωρήσει στη συνέχεια θα εξαρτηθεί από το πώς θα εξελιχθεί η AI τα επόμενα χρόνια, από το πόσο ακριβή θα είναι η πρόσβαση σε αυτήν και από το πώς θα πάει αυτό το εργαστήριο.
Τα μαθηματικά περνούν τη μεγαλύτερη αλλαγή στην ιστορία τους
Η Hang Lu Su από το Imperial College London είναι μία από τις ερευνήτριες που συμμετέχουν στο εργαστήριο. Χρησιμοποίησε το ChatGPT για να μάθει το Lean μόλις πριν από έξι μήνες και τώρα εργάζεται εδώ στην αιχμή της έρευνας.
Οι περισσότεροι μαθηματικοί που γνωρίζει εξακολουθούν να χρησιμοποιούν χαρτί και μολύβι, οπότε η χρήση 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.
