Μια από τις πιο δύσκολες ανοιχτές ερωτήσεις της μαθηματικής φυσικής απέκτησε, σύμφωνα με την OpenAI, μια απάντηση από σύστημα τεχνητής νοημοσύνης. Η εταιρεία δημοσίευσε στις 8 Σεπτεμβρίου μια αναλυτική απόδειξη και μια τυποποιημένη εκδοχή της σε Lean για το πρόβλημα ύπαρξης και ομαλότητας των εξισώσεων Navier–Stokes.
Η ανακοίνωση δεν σημαίνει ότι η μαθηματική κοινότητα έχει ήδη απονείμει το έπαθλο ή ότι η απόδειξη έχει περάσει ανεξάρτητη αξιολόγηση. Σημαίνει ότι η OpenAI υποστηρίζει πως το εσωτερικό της σύστημα κατασκεύασε ένα αντιπαράδειγμα: μια αρχικά ομαλή ροή που εμφανίζει ανωμαλία σε πεπερασμένο χρόνο, με πεπερασμένη ενέργεια σε όλη την εξέλιξη.
Τι ρωτά το πρόβλημα Navier–Stokes
Οι εξισώσεις Navier–Stokes περιγράφουν την κίνηση των ρευστών ως συνεχών μέσων. Χρησιμοποιούνται σε εφαρμογές από τον σχεδιασμό αεροσκαφών και την πρόγνωση του καιρού έως τη μελέτη της ροής του αίματος. Η δυσκολία δεν βρίσκεται στο να γραφτούν οι εξισώσεις, αλλά στο να αποδειχθεί τι μπορούν να κάνουν οι λύσεις τους σε τρεις διαστάσεις.
Για ένα ασυμπίεστο ρευστό σταθερής πυκνότητας, το ερώτημα είναι αν μια ομαλή αρχική κατάσταση παραμένει ομαλή για πάντα. «Ανωμαλία» σημαίνει εδώ ότι η ταχύτητα μπορεί να αυξηθεί χωρίς φραγμό μέσα σε πεπερασμένο χρόνο. Το ιξώδες τείνει να εξομαλύνει την κίνηση, όμως οι μη γραμμικοί όροι μπορούν να ενισχύσουν τις διακυμάνσεις με τρόπο που δεν έχουμε καταφέρει ακόμη να ελέγξουμε πλήρως.
Το πρόβλημα έχει τις ρίζες του στην εργασία των Claude-Louis Navier και George Gabriel Stokes τον 19ο αιώνα. Ο Jean Leray απέδειξε το 1934 ότι υπάρχουν λύσεις με γενικευμένη έννοια, αλλά το αν αυτές παραμένουν ομαλές έγινε κεντρικό αναπάντητο ερώτημα. Το 2000, το Clay Mathematics Institute το συμπεριέλαβε στα επτά Millennium Prize Problems.
Τι ακριβώς ισχυρίζεται η OpenAI
Η OpenAI λέει ότι το σύστημά της παρήγαγε αναλυτική απόδειξη για τη δημιουργία ανωμαλίας σε πεπερασμένο χρόνο και ότι η ίδια απόδειξη τυποποιήθηκε σε Lean. Η κατασκευή ξεκινά από ρευστό σε ηρεμία, στο οποίο εφαρμόζεται μια ομαλή δύναμη. Η ενέργεια παραμένει πεπερασμένη, ενώ η ταχύτητα αυξάνεται χωρίς φραγμό καθώς σχηματίζεται η ανωμαλία.
Η γεωμετρική εικόνα είναι ένας στρόβιλος που σπειροειδώς συγκλίνει και επιμηκύνεται, σαν λεπτό κορδόνι. Η κεντρική περιοχή μικραίνει και η ροή επιταχύνεται. Το κρίσιμο σημείο, σύμφωνα με την ανακοίνωση, είναι ότι η κατάρρευση προκύπτει από τη δυναμική των εξισώσεων και όχι από την επιβολή μιας άπειρης εξωτερικής δύναμης.
Με πιο τεχνικούς όρους, οι όροι που περιγράφουν την επιτάχυνση, τις διαφορές πίεσης, τη μεταφορά ορμής και το ιξώδες γίνονται μεγάλοι, αλλά αλληλοαναιρούνται με ακριβή τρόπο. Έτσι, η εξωτερική δύναμη παραμένει ομαλή την ίδια στιγμή που η ταχύτητα της ροής αυξάνεται χωρίς φραγμό.
Η ανακοίνωση υποστηρίζει ότι αυτό επιλύει το πρόβλημα, επειδή εγκαθιστά τις δηλώσεις C και D της επίσημης διατύπωσης του Clay Institute. Η OpenAI, ωστόσο, δηλώνει ρητά ότι δεν σκοπεύει να διεκδικήσει το Millennium Prize για το αποτέλεσμα.
Πώς χρησιμοποιήθηκαν οι agents
Για την αναζήτηση της λύσης, η OpenAI χρησιμοποίησε ένα εσωτερικό σύστημα συντονισμένων agents με πρόσβαση σε αποθηκευμένη έκδοση του διαδικτύου και σε εργαλεία εκτέλεσης κώδικα. Οι agents χωρίστηκαν σε ομάδες που επικοινωνούσαν μεταξύ τους και εξερεύνησαν διαφορετικές εκδοχές του προβλήματος: άλλες θα οδηγούσαν σε απόδειξη και άλλες σε διάψευση.
Σύμφωνα με την εταιρεία, η ομάδα που εργάστηκε στη Navier–Stokes περιλάμβανε περίπου 10.000 ταυτόχρονους agents. Η πρώτη λύση προέκυψε περίπου 88 ώρες μετά την έναρξη της προσπάθειας, στις 5 Σεπτεμβρίου. Η τυποποίηση και η επαλήθευση σε Lean χρειάστηκαν ακόμη 17 ώρες μέσω του GPT‑6 Astra, όπως αναφέρει η ίδια πηγή.
Συνολικά, οι agents έστειλαν 4,9 εκατομμύρια μηνύματα και παρήγαγαν περίπου 300 δισεκατομμύρια tokens για τα προβλήματα που εξετάστηκαν. Για τη Navier–Stokes, η OpenAI αναφέρει 2,7 εκατομμύρια μηνύματα και περίπου 130 δισεκατομμύρια tokens. Οι αριθμοί δείχνουν την κλίμακα του πειράματος, όχι από μόνοι τους την ορθότητα της απόδειξης.
Η Lean formalization δεν κλείνει μόνη της τη συζήτηση
Η τυποποίηση σε Lean είναι σημαντικό πλεονέκτημα, επειδή μεταφράζει τα βήματα σε μορφή που μπορεί να ελεγχθεί από proof assistant. Δεν αντικαθιστά όμως την ανεξάρτητη εξέταση των ορισμών, των προϋποθέσεων και της αντιστοίχισης ανάμεσα στο τυπικό κείμενο και στο αρχικό μαθηματικό claim.
Ακόμη πρέπει να εξεταστεί αν η κατασκευή ικανοποιεί ακριβώς την επίσημη διατύπωση του Clay Institute, αν όλα τα βήματα της αναλυτικής απόδειξης είναι έγκυρα και αν η Lean formalization καλύπτει το ουσιώδες επιχείρημα χωρίς κρυφές ασυνέπειες. Η δημοσίευση της OpenAI περιλαμβάνει το paper και σύνδεσμο προς τον κώδικα της τυποποίησης, ώστε η διαδικασία να μπορεί να ελεγχθεί από άλλους μαθηματικούς.
Αυτό είναι και το όριο της είδησης: πρόκειται για εξαιρετικά σημαντικό ισχυρισμό που έχει δημοσιοποιηθεί με υλικό προς αξιολόγηση, όχι για αποτέλεσμα που έχει ήδη επικυρωθεί από ανεξάρτητους ειδικούς. Στα μαθηματικά, η αναπαραγωγή, η κριτική ανάγνωση και η αποδοχή από την κοινότητα είναι μέρος της ίδιας της απόδειξης στην πράξη.
Γιατί η εξέλιξη έχει σημασία για την AI
Αν επιβεβαιωθεί, το αποτέλεσμα θα είναι κάτι περισσότερο από ένα ακόμη εντυπωσιακό benchmark. Θα δείχνει ότι ένα σύστημα μπορεί να συνδυάσει εξερεύνηση πολλών υποθέσεων, συνεργασία agents, παραγωγή αναλυτικού επιχειρήματος και τυπική επαλήθευση σε ένα πρόβλημα όπου η ανθρώπινη έρευνα έχει προχωρήσει αργά για δεκαετίες.
Παράλληλα, η υπόθεση υπενθυμίζει γιατί η AI στην επιστήμη χρειάζεται διαφάνεια και αυστηρούς ελέγχους. Η ταχύτητα παραγωγής μιας πιθανής λύσης μπορεί να αυξάνεται δραματικά, όμως η αξία της εξαρτάται από το αν η λύση αντέχει σε ανεξάρτητο έλεγχο. Για την ώρα, το επόμενο κρίσιμο βήμα δεν είναι ένας μεγαλύτερος αριθμός agents, αλλά η προσεκτική αξιολόγηση της απόδειξης από τη μαθηματική κοινότητα.
Πηγή: OpenAI — On the Navier–Stokes Millennium Prize Problem.