Το AI της Axiom Math Επαληθεύει το Θεώρημα των 246 Κενού Πριμών στο Lean

Η Axiom Math δηλώνει ότι το σύστημα AxiomProver της παρήγαγε μια μηχανικά ελεγμένη απόδειξη Lean 4 για το ισχυρότερο γνωστό αποτέλεσμα σχετικά με τα κενά μεταξύ πρώτων αριθμών: το θεώρημα που λέει ότι άπειρα ζεύγη πρώτων διαφέρουν κατά όχι περισσότερο από 246. Η εταιρεία δημοσίευσε το αποτέλεσμα στις 17 Αυγούστου 2026 ως ένα διαδραστικό σχέδιο τυποποίησης, αποδοχόμενο 41 ονομαστικούς μαθηματικούς, μηχανικούς και κύριους ερευνητές, με Το IEEE Spectrum πρώτα ανέφερε το ορόσημο.

Το όριο 246 αποτελεί το τρέχον άκρο της ανθρώπινης γνώσης στην μακρά επίθεση στη υπόθεση των δίδυμων πρώτων, τη θεωρία του 19ου αιώνα που υποστηρίζει ότι πρώτοι αριθμοί χωρισμένοι ακριβώς κατά δύο επαναλαμβάνονται επ’ άπειρον. Η Σελίδα έργου της Axiom Math περιγράφει την εργασία ως ενιαία τυποποίηση του άρθρου του James Maynard του 2013 «Small gaps between primes» μαζί με το τμήμα της συνέχειας της συνεργασίας Polymath8b που συνέδεσε το όριο του Maynard από 600 σε 246. Οι μηχανικά ελεγμένες αποδείξεις οργανώνονται σε μια δημόσια βιβλιοθήκη Lean, PrimeGapsLib, με το θεώρημα 246 ως το κύριο αποτέλεσμα.

«Αυτό το θεώρημα αντιπροσωπεύει αυτή τη στιγμή το όριο της ανθρώπινης γνώσης για τους πρώτους αριθμούς», είπε ο Ken Ono, ιδρυτικός μαθηματικός της Axiom Math.

Η τυπική επαλήθευση σημαίνει τη μετάφραση μιας απόδειξης σε μια γλώσσα που ένα μικρό, αξιόπιστο πρόγραμμα, το λεγόμενο πυρήνα, μπορεί να ελέγξει γραμμή προς γραμμή. Το αποτέλεσμα δεν αποτελεί απόλυτη εγγύηση — η δήλωση πρέπει να μεταφραστεί σωστά και ο ελεγκτής πρέπει να είναι αξιόπιστος — αλλά αφαιρεί την ανθρώπινη ευπάθεια από την αλυσίδα. Μέχρι τώρα, τα συστήματα AI που ανταγωνίζονται σε μαθηματικά benchmarks έχουν κυρίως αξιολογηθεί σε προβλήματα διαγωνισμών με σύντομες, αυτόνομες αποδείξεις· το χάσμα μεταξύ αυτών των αποτελεσμάτων και της τυποποίησης επιπέδου έρευνας ήταν μεγάλο, ένα μοτίβο ορατό σε προηγούμενα συστήματα που διαπρέπουν στη γεωμετρία ολυμπιακών διαγωνισμών.

Από 70 εκατομμύρια σε 246

Η ίδια η υπόθεση, διατυπωμένη ακριβώς από τον Alphonse de Polignac τον 19ο αιώνα, παραμένει αδίκητη. Το πρώτο πεπερασμένο όριο οποιουδήποτε είδους εμφανίστηκε το 2013, όταν ο Yitang Zhang απέδειξε ότι άπειρα ζεύγη πρώτων βρίσκονται εντός 70 εκατομμυρίων μεταξύ τους. Μήνες αργότερα, ο Maynard παρουσίασε μια βελτιωμένη μέθοδο φίλτρου και μείωσε το όριο σε 600 — εργασία που συνέβαλε στο μετάλλι του Fields 2022 — και η συνεργασία Polymath8b, που περιελάμβανε τους Maynard και Terence Tao, το έσυρε σε 246. Το σχέδιο της Axiom Math παρουσιάζει αυτή την εξέλιξη ως το έργο που προχώρησε στην τυποποίηση.

Η τυποποίηση ακολουθεί μια αλυσίδα εργασιών που η εταιρεία περιγράφει σε τρία στάδια. Οι ερευνητές πρώτα συνέγραψαν την απόδειξη ως σχέδιο — κάθε ορισμός, λήμμα και θεώρημα με ετικέτα, ακριβή δήλωση και λίστα των αποτελεσμάτων από τα οποία εξαρτάται — δημιουργώντας ένα γράφημα εξαρτήσεων που διέταξε τη δουλειά. Το AxiomProver, το πολυ‑πρακτορικό σύστημα της εταιρείας για μαθηματική έρευνα μέσω τυπικής απόδειξης, στη συνέχεια παρήγαγε μηχανικά ελεγμένες αποδείξεις Lean 4 βασισμένες στο Mathlib, τη βιβλιοθήκη μαθηματικών της κοινότητας, και στο PrimeNumberTheoremAnd, το υπάρχον έργο τυποποίησης υπό την ηγεσία του Alex Kontorovich και του Tao. Η ομάδα της Axiom στη συνέχεια εξέτασε τον παραγόμενο κώδικα και τον οργάνωσε σε PrimeGapsLib.

Τα κύρια αποτελέσματα που αναφέρει η βιβλιοθήκη υπερβαίνουν ελαφρώς το κεντρικό θεώρημα. Πέρα από το όριο 246, τυποποιεί το όριο 600 του Maynard, και περιλαμβάνει μια αυτόνομη πρόκληση επαλήθευσης — χτισμένη μόνο πάνω στο Mathlib, με το κενό της απόδειξης κενό — που επιτρέπει σε όποιον διαθέτει το εργαλείο συγκριτή Lean να επιβεβαιώσει ανεξάρτητα ότι οι αποδείξεις της βιβλιοθήκης ταιριάζουν με τα δηλωμένα θεωρήματα. Η εταιρεία προειδοποιεί ότι ο πλήρης έλεγχος μπορεί να διαρκέσει ώρες· μια μειωμένη έκδοση που καλύπτει τα άλλα δύο αποτελέσματα εκτελείται σε λεπτά.

Πού Τοποθετείται Αυτό Μεταξύ των Αξιώσεων Τυποποίησης AI

Το αποτέλεσμα εμφανίζεται σε μια χρονιά αυξανόμενων αξιώσεων σχετικά με συστήματα AI που εκτελούν μαθηματική έρευνα, οι περισσότερες από τις οποίες στηρίζονται σε βαθμολογίες διαγωνισμών ή σύντομες αποδείξεις. Η Axiom Math ήταν μία από τις πιο επιθετικές αξιώσεις: το AxiomProver αποδίδεται με την επίλυση προηγουμένως ανοιχτών προβλημάτων, συμπεριλαμβανομένης της εργασίας που η εταιρεία έχει δημοσιεύσει σε επιστημονικά περιοδικά, και τα συστήματα AI έχουν πλέον λύσει αρκετά μακροχρόνια προβλήματα του Erdős. Η τυποποίηση 246 αποτελεί διαφορετικό είδος αποτελέσματος — όχι νέο θεώρημα, αλλά μια μηχανικά ελεγμένη ανακατασκευή μιας από τις πιο τεχνικά απαιτητικές αποδείξεις στη σύγχρονη θεωρία αριθμών.

Η πιο κοντινή σύγκριση είναι νωρίτερα φέτος, όταν η Math, Inc. χρησιμοποίησε τον πράκτορα Gauss για να ολοκληρώσει την τυπική απόδειξη των βραβευμένων με το Μετάλλιο Fields αποτελεσμάτων συσσωμάτωσης σφαίρας της Maryna Viazovska σε διαστάσεις 8 και 24. Ο Sidharth Hariharan, φοιτητής διδακτορικού στο Carnegie Mellon που ηγήθηκε της ανθρώπινης προσπάθειας σχεδίου σε αυτήν την τυποποίηση και τώρα είναι πρακτική στην Axiom Math και ονομαστικός μαθηματικός συνεισφέρων στο έργο 246, υποστηρίζει ότι το νέο αποτέλεσμα είναι η πιο ολοκληρωμένη επίτευξη. Η λογική του, όπως την περιέγραψε, είναι ότι η Axiom δημιουργήθηκε για επαναχρησιμοποίηση: αντί για μια εφάπαξ τυποποίηση μιας μόνο απόδειξης, η PrimeGapsLib είναι μια συντηρούμενη βιβλιοθήκη αποτελεσμάτων κενών πρώτων που προορίζεται να υποστηρίξει μελλοντική εργασία τυποποίησης και έρευνα.

Αυτή η διάκριση έχει σημασία για το πώς πρέπει να διαβαστεί το αποτέλεσμα. Μία εφάπαξ επαλήθευση δείχνει ότι ένα σύστημα μπορεί να αντιμετωπίσει μια δύσκολη απόδειξη. Μια βιβλιοθήκη δείχνει κάτι πιο κοντά σε υποδομή — επαναχρησιμοποιήσιμη τυπική μηχανή που άλλα αποτελέσματα μπορούν να αξιοποιήσουν — που είναι η κατεύθυνση που τα συστήματα τυπικής απόδειξης έχουν προχωρήσει καθώς μεταβαίνουν από την επίλυση ασκήσεων στην επαλήθευση πραγματικών μαθηματικών. Η αξίωση δυνατότητας εδώ βασίζεται σε αντικείμενα που είναι δημόσια και επαναεκτελέσιμα αντί για βαθμολογία benchmark: το σχέδιο, ο κώδικας Lean και μια πρόκληση συγκριτή σχεδιασμένη ώστε εξωτερικοί ερευνητές να μπορούν να επαληθεύσουν τις αποδείξεις μόνοι τους.

Ο Ono θέτει τα μαθηματικά ως δοκιμαστικό πεδίο για μια μεγαλύτερη φιλοδοξία. Εάν οι ιδιότητες του λογισμικού — είτε ένα πρόγραμμα τερματίζει, είτε η έξοδό του είναι σωστή για κάθε είσοδο — μπορούν να εκφραστούν ως ακριβείς μαθηματικές δηλώσεις, τότε τα συστήματα που προέρχονται από το AxiomProver θα μπορούσαν να τις αποδείξουν τυπικά, υποστηρίζει, δείχνοντας προς την επαλήθευση του κώδικα που παράγεται από AI και αρχίζει να τρέχει σε υποδομές, χρηματοοικονομικά και συστήματα ασφαλείας.

«Ο κόσμος πρόκειται να λειτουργεί με κώδικα υπολογιστών που κανείς δεν έχει διαβάσει», είπε ο Ono. «Η AI είναι εδώ και δεν μπορούμε πλέον να κοιτάμε μακριά — η τυποποίηση αποδείξεων είναι ένα δοκιμαστικό πεδίο για την επίλυση αυτού που θεωρώ ότι είναι η πιο σημαντική πρόκληση που θα αντιμετωπίσουμε από την AI.»

Προς το παρόν το παραδοτέο είναι πιο περιορισμένο και ελέγξιμο: ένα σχέδιο με 41 συγγραφείς, μια δημόσια βιβλιοθήκη Lean και μια μηχανικά επαληθευμένη απόδειξη ότι οι πρώτοι αριθμοί εντός 246 μεταξύ τους δεν εξαντλούνται ποτέ — ο πιο κοντινός επαληθευμένος γείτονας της υπόθεσης των δίδυμων πρώτων, και το πιο βαθύ κομμάτι ερευνητικών μαθηματικών που ένα σύστημα AI έχει ελέγξει μέχρι τώρα από άκρη σε άκρη.