Η μεγάλη απόδειξη της OpenAI για το περίφημο πρόβλημα Navier-Stokes βρίσκεται ξανά υπό αμφισβήτηση. Τρεις μαθηματικοί εντόπισαν διαφορές ανάμεσα στη μαθηματική απόδειξη που δημοσίευσε η εταιρεία και στην έκδοση σε Lean, που προορίζεται για την αυτόματη επαλήθευση της λογικής της.
Το εύρημα δεν αποδεικνύει ότι η μαθηματική απόδειξη της OpenAI είναι λανθασμένη. Αναδεικνύει, όμως, ένα ουσιαστικό πρόβλημα: ακόμη και όταν ένα σύστημα επαλήθευσης δέχεται έναν μαθηματικό ισχυρισμό ως έγκυρο, αυτό δεν σημαίνει απαραίτητα ότι ελέγχει ακριβώς το ίδιο επιχείρημα που διαβάζει ένας άνθρωπος.
Δύο διαφορετικές εκδοχές της ίδιας απόδειξης
Στις 8 Σεπτεμβρίου 2026, η OpenAI ανακοίνωσε ότι ένα εσωτερικό μοντέλο της παρήγαγε μια απόδειξη για τον σχηματισμό μαθηματικής ανωμαλίας σε πεπερασμένο χρόνο στις εξισώσεις Navier-Stokes. Το πρόβλημα αφορά τη συμπεριφορά των εξισώσεων που περιγράφουν την κίνηση των ρευστών και αποτελεί ένα από τα μεγάλα άλυτα προβλήματα των μαθηματικών.
Η OpenAI δημοσίευσε δύο εκδοχές του αποτελέσματος. Η μία ήταν κείμενο με μαθηματικούς συμβολισμούς γραμμένο ώστε να διαβάζεται από ανθρώπους. Η δεύτερη έκδοση ήταν μια τυποποιημένη εκδοχή σε Lean, μια γλώσσα που χρησιμοποιείται για την επίσημη επαλήθευση μαθηματικών αποδείξεων.
Η δεύτερη εκδοχή έχει μεγάλη σημασία επειδή επιτρέπει στον υπολογιστή να ελέγξει αν το διατυπωμένο μαθηματικό επιχείρημα ακολουθεί τους κανόνες του συστήματος. Για να επιβεβαιώσει, όμως, την αρχική απόδειξη, πρέπει να αναπαριστά πιστά το περιεχόμενό της. Και αυτό ακριβώς αμφισβητούν οι ερευνητές.
Τα ευρήματα των μαθηματικών
Στην εργασία τους, με τίτλο Navier-Stokes lost in translation, οι Alexander Bastounis, Fabian Circelli και Anders C. Hansen παρουσιάζουν παραδείγματα στα οποία η τυποποιημένη απόδειξη σε Lean αποκλίνει από το αρχικό κείμενο.
Σε ένα από αυτά, η γραπτή απόδειξη αναφέρει πως για να ισχύει μια συγκεκριμένη εκτίμηση απαιτούνται τέσσερις επιπλέον παράγωγοι μιας συνάρτησης. Στον κώδικα Lean όμως, η αντίστοιχη διατύπωση απαιτεί πέντε. Έτσι, η έκδοση που ελέγχει ο υπολογιστής είναι ασθενέστερη σε σχέση με αυτή που δηλώνει το αρχικό κείμενο.
Οι ερευνητές εντοπίζουν επίσης διαφορές στη διατύπωση και στην απόδειξη μιας εκτίμησης που αφορά τη ροή πίεσης. Το πρόβλημα, επομένως, δεν είναι ότι το Lean απέτυχε να ελέγξει τον κώδικα. Είναι ότι ο κώδικας που ελέγχθηκε δεν αποδίδει πιστά ορισμένα σημεία της μαθηματικής απόδειξης που δημοσιεύτηκε για ανθρώπους.
Η σημασία αυτών για την AI
Η τυπική επαλήθευση θεωρείται ένα από τα ισχυρότερα εργαλεία για τον έλεγχο μαθηματικών αποτελεσμάτων που παράγονται από AI. Σε αντίθεση με μια απλή απάντηση chatbot, ο κώδικας Lean μπορεί να ελεγχθεί μηχανικά για να διαπιστωθεί αν μια συγκεκριμένη διατύπωση αποδεικνύεται με βάση τους κανόνες του συστήματος.
Πρόκειται για ένα πολύ χρήσιμο εργαλείο, όμως προϋποθέτει η έκδοση σε Lean να είναι ακριβώς ίδια με αυτή που έχουμε στο αρχικό κείμενο. Σε περίπτωση που η εκδοχή σε Lean δεν είναι ακριβώς ίδια, η απόδειξη πρέπει να ακυρωθεί και να ξαναγραφτεί ώστε να έχει πλήρη ταύτιση με το αρχικό κείμενο.
Οι τρεις ερευνητές δεν υποστηρίζουν ότι η γραπτή απόδειξη της OpenAI είναι λανθασμένη. Το συμπέρασμά τους είναι πιο συγκεκριμένο: η τυποποιημένη εκδοχή της δεν αρκεί για να επιβεβαιώσει την ορθότητά της.
Με τη ματιά του Techmaniacs
Το αποτέλεσμα της OpenAI εξακολουθεί να απαιτεί ανεξάρτητο μαθηματικό έλεγχο, όπως κάθε ισχυρισμός στον χώρο της έρευνας. Το ότι όμως η εκδοχή σε Lean ήταν διαφορετική είναι ένα μεγάλο παράπτωμα, που δεν θα έπρεπε να έχει συμβεί εξ αρχής.
Δεν γνωρίζουμε αν αυτές οι διαφορές έγιναν κατά λάθος ή επίτηδες, ώστε να δείξει η OpenAI πως η τεχνητή νοημοσύνη της τα κατάφερε, όμως μέχρι να υπάρξει πλήρης μαθηματική επιβεβαίωση, εμείς δεν μπορούμε να θεωρήσουμε πως η τεχνητή νοημοσύνη έδωσε μια λύση σε ένα μαθηματικό πρόβλημα δεκαετιών.
