Η Axiom Math κυκλοφορεί απόδειξη 43,1 εκατομμυρίων γραμμών στο Lean για την ταξινόμηση των ομάδων

Η Axiom Math δήλωσε στις 27 Οκτωβρίου 2026 ότι κυκλοφορεί αυτό που αποκαλεί την πρώτη πλήρη απόδειξη της Ταξινόμησης των Πεπερασμένων Απλών Ομάδων που έχει ελεγχθεί από υπολογιστή. Η απόδειξη δημιουργήθηκε μέσα σε 24 ημέρες από μηχανικούς και μαθηματικούς, οι οποίοι συντόνισαν δεκάδες σμήνη πρακτόρων τεχνητής νοημοσύνης που έγραψαν περίπου 43,1 εκατομμύρια γραμμές κώδικα στον βοηθό αποδείξεων Lean.

«Σήμερα κυκλοφορούμε την πρώτη πλήρη απόδειξη της Ταξινόμησης των Πεπερασμένων Απλών Ομάδων (CFSG) που έχει ελεγχθεί από υπολογιστή», έγραψε η εταιρεία στην ανακοίνωσή της. Η ταξινόμηση προσδιορίζει τα βασικά δομικά στοιχεία των πεπερασμένων ομάδων, ενώ η αρχική της απόδειξη εκτείνεται σε περίπου 15.000 σελίδες, κατανεμημένες σε περισσότερα από 500 άρθρα από περίπου 100 μαθηματικούς. Το μέγεθός της τής χάρισε το προσωνύμιο «τεράστιο θεώρημα».

Τι κυκλοφόρησε η Axiom

Η CFSG αποδεικνύει ότι κάθε πεπερασμένη απλή ομάδα είναι κυκλική και έχει πρώτο πλήθος στοιχείων, είναι εναλλάσσουσα σε τουλάχιστον πέντε σύμβολα, ανήκει σε μία από τις δεκαέξι άπειρες οικογένειες ομάδων τύπου Lie που κατασκευάζονται πάνω σε πεπερασμένα σώματα ή είναι μία από ακριβώς 26 μεμονωμένες σποραδικές ομάδες· η ανακοίνωση σημειώνει ότι ορισμένοι συγγραφείς μετρούν την ομάδα Tits ως 27η. Η μεγαλύτερη σποραδική ομάδα, η Monster, κατασκευάστηκε από τον Robert Griess το 1980 με τη χρήση άλγεβρας διάστασης 196.884.

Η ανθρώπινη προσπάθεια για την απόδειξη διήρκεσε δεκαετίες. Το 1963, οι Walter Feit και John Thompson απέδειξαν ότι κάθε μη αβελιανή πεπερασμένη απλή ομάδα έχει άρτια τάξη, σε μια εργασία 255 σελίδων που κάλυψε ολόκληρο τεύχος του Pacific Journal of Mathematics. Το 1972, ο Daniel Gorenstein παρουσίασε ένα πρόγραμμα δεκαέξι βημάτων για την ολοκλήρωση της ταξινόμησης και το 1983 δήλωσε ότι αυτή είχε ολοκληρωθεί. Ωστόσο, η περίπτωση των quasithin ομάδων βασιζόταν σε ημιτελές χειρόγραφο του Geoffrey Mason, έως ότου οι Michael Aschbacher και Stephen Smith δημοσίευσαν το 2004 μια μελέτη 1.221 σελίδων, ολοκληρώνοντας αυτό που έγινε γνωστό ως απόδειξη πρώτης γενιάς. Μια πιο συστηματική απόδειξη δεύτερης γενιάς, την οποία ξεκίνησαν οι Gorenstein και Richard Lyons και στην οποία προστέθηκαν αργότερα οι Ronald Solomon και Inna Capdeboscq, παραμένει ανολοκλήρωτη· γι’ αυτό η Axiom τυποποίησε την απόδειξη πρώτης γενιάς.

Η σελίδα του έργου παρουσιάζει την τυποποίηση ως πιστή στην απόδειξη πρώτης γενιάς, με κάθε λογικό βήμα να ελέγχεται από τον πυρήνα του Lean, και αναφέρει ότι περιλαμβάνει 43,1 εκατομμύρια γραμμές Lean, 2,05 εκατομμύρια δηλώσεις και 715 εργασίες και βιβλία. Η Axiom αναφέρει ότι ο χάρτης της απόδειξης βασίστηκε στους τόμους της απόδειξης δεύτερης γενιάς και ότι η τυποποίηση ενσωματώνει περίπου 1,2 εκατομμύρια γραμμές κώδικα από το προγενέστερο έργο Qiuzhen-CFSG και στηρίζεται στο Mathlib, για το οποίο αποδίδει τα εύσημα σε εκατοντάδες συνεισφέροντες. Ως βασικούς συντελεστές του έργου κατονομάζει τους Dean Cureton, Vasily Ilin, Bhavik Mehta και Niels Voss, με κύριο ερευνητή τον Letong Hong.

Το δημόσιο αποθετήριο στο GitHub περιγράφει το αποτέλεσμα ως απόδειξη Lean4 χωρίς χρήση του sorry, βασισμένη στην έκδοση 4.35.0-rc3, χτισμένη πάνω στο Mathlib και στο έργο TauCeti και χρησιμοποιώντας μόνο τα τυπικά αξιώματα Classical.choice, propext και Quot.sound, χωρίς native_decide. Η τυπική διατύπωση της ταξινόμησης, η οποία προέρχεται από το TauCeti, είναι η εξής: «Κάθε πεπερασμένη απλή ομάδα είναι ισόμορφη με μία από τις ομάδες που έχουν κατασκευαστεί ρητά στον κατάλογο ταξινόμησης». Το αρχείο README αναφέρει ότι η εντολή lake build ελέγχει ολόκληρη την ανάπτυξη και ότι οι ανοικτές αλλαγές στο εργαλείο κατασκευής Lake, καθώς και οι βελτιστοποιήσεις που σκοπεύει να συνεισφέρει η ομάδα στο αρχικό έργο, μείωσαν τον χρόνο κατασκευής κάτω από τις 24 ώρες· ο κώδικας διατίθεται με άδεια Apache-2.0.

Προσπάθεια 24 ημερών με σμήνος πρακτόρων

Την 1η Οκτωβρίου 2026, η Axiom άνοιξε ένα κανάλι στο Slack για τον συντονισμό του έργου. Η προϋπάρχουσα εργασία στο Lean και ένας εσωτερικός χάρτης της απόδειξης, που καταρτίστηκε με βάση τη δημοσιευμένη βιβλιογραφία, χώρισαν την προσπάθεια σε 108 ορόσημα και περίπου 380 μικρότερες εργασίες. Το πρώτο σμήνος τέθηκε σε λειτουργία στις 2 Οκτωβρίου 2026, με τους πράκτορες να αναλαμβάνουν ορόσημα μέσω ζητημάτων στο GitHub και να αναφέρουν στο Slack την ολοκλήρωση των εργασιών τους. Οι επικεφαλής πράκτορες ανέλυαν τα δύσκολα επιχειρήματα σε επιμέρους βήματα και εξέταζαν τις διατυπώσεις, ενώ άλλοι πράκτορες αναζητούσαν υπάρχοντα αποτελέσματα ή έγραφαν αποδείξεις στο Lean. Ένας πράκτορας μπορούσε επίσης να αναθέσει σε άλλους την αναζήτηση ελλειπουσών προϋποθέσεων, με τα αποτελέσματά τους να προστίθενται σε ένα κοινόχρηστο αποθετήριο.

Η αρχική πρόοδος ανέδειξε αδύναμα σημεία. Ορισμένα ορόσημα που έμοιαζαν διαχειρίσιμα έκρυβαν τεράστιες προϋποθέσεις, τις οποίες οι πράκτορες είχαν θεωρήσει δεδομένες αντί να τις αποδείξουν. Η ομάδα διέγραψε δεκάδες χιλιάδες γραμμές που βασίζονταν σε αυτές τις παραδοχές και ξεκίνησε ξανά με πιο στέρεο σχέδιο. Ένα από τα πρώτα ορόσημα αφορούσε το θεώρημα του συναρτητή signalizer, του οποίου η υποψήφια απόδειξη στηριζόταν σε δομικές παραδοχές που έπρεπε ακόμη να αιτιολογηθούν. Οι χρόνοι κατασκευής έγιναν επίσης σημείο συμφόρησης, καθώς οι πράκτορες παρήγαν αποδείξεις ταχύτερα απ’ όσο μπορούσε το Lean να τις επανελέγξει. Η Axiom αναφέρει ότι οι μηχανικοί της διένειμαν τα αποθηκευμένα αποτελέσματα κατασκευής σε υπολογιστικούς κόμβους, εκτελούσαν ανεξάρτητους ελέγχους παράλληλα και μετέφεραν τους δαπανηρούς πεπερασμένους υπολογισμούς σε πιστοποιητικά που μπορούσαν να ελεγχθούν χωριστά· σύμφωνα με την εταιρεία, οι αλλαγές αυτές επιτάχυναν την επαλήθευση κατά τάξεις μεγέθους.

Στις 10 Οκτωβρίου 2026, ένα μήνυμα στο κανάλι ανακοίνωσε ότι οι πράκτορες είχαν αποδείξει πως η Monster είναι απλή, αναφέρει η εταιρεία. Οι πράκτορες τυποποίησαν επίσης την ύπαρξη της Monster μέσω της άλγεβρας Griess, καθώς και ένα θεώρημα που ταυτοποιεί τις ομάδες τύπου Monster με τη Monster. Στις 13 Οκτωβρίου 2026, ολοκληρώθηκε μόνο ένα ορόσημο και οι μηχανικοί οργάνωσαν μια προσπάθεια ανασχεδιασμού, χωρίζοντας τα ανολοκλήρωτα ορόσημα σε μικρότερα, επακριβώς διατυπωμένα θεωρήματα. Για κάθε τέτοια διάσπαση έπρεπε να αποδεικνύεται, μέσω μιας σύντομης απόδειξης στο Lean, πώς τα επιμέρους μέρη θα τεκμηρίωναν το αρχικό ορόσημο.

Κενά που εντοπίστηκαν στη δημοσιευμένη απόδειξη

Η μετάφραση της απόδειξης σε Lean αποκάλυψε προβλήματα στα δημοσιευμένα επιχειρήματα, αναφέρει η Axiom. Τα περισσότερα ήταν μικρής έκτασης — τυπογραφικά λάθη, σφάλματα σε πίνακες ή παραλειπόμενες υποθέσεις —, αλλά η εταιρεία καταγράφει 34 αξιοσημείωτες αποκλίσεις από τη δημοσιευμένη εκδοχή, με σημαντικότερη εκείνη που αφορά το Θεώρημα μη ισορροπημένων ομάδων (Unbalanced Group Theorem, UGT).

Ένα παράδειγμα εντοπίστηκε στους τόμους των Aschbacher και Smith για τις οιονεί λεπτές ομάδες, όπου ένα λήμμα υποστήριζε ότι δύο αριθμητικά μεγέθη ήταν ίσα. Οι πράκτορες εντόπισαν ένα αντιπαράδειγμα που αφορούσε την ομάδα SL₂(5), στην οποία το ένα μέγεθος ήταν 1, ενώ η υποτιθέμενη ισότητα απαιτούσε να είναι 2. Η αντικατάσταση της ισότητας με μια ανισότητα διόρθωσε το λήμμα, αλλά μεταγενέστερα επιχειρήματα είχαν χρησιμοποιήσει την ισότητα για να αποκλείσουν περιπτώσεις, οπότε η ομάδα διεύρυνε ένα προηγούμενο επιχείρημα ώστε να καλύπτει και αυτές τις διαμορφώσεις.

Το UGT συμβάλλει στον προσδιορισμό μιας ολόκληρης ομάδας με βάση πληροφορίες για τις υποομάδες της: σύμφωνα με την περίληψη της συνοδευτικής δημοσίευσης, υπό τις επαγωγικές υποθέσεις της ταξινόμησης, αν μια μη τετριμμένη υποομάδα περιττής τάξης είναι κανονική στον κεντροποιητή μιας involution, τότε η ευρύτερη απλή ομάδα είναι είτε ομάδα τύπου Lie σε περιττή χαρακτηριστική είτε εναλλάσσουσα ομάδα ορισμένων βαθμών. Η Axiom προσέγγισε το UGT μέσω της μονογραφίας του John Walter του 1986 και, κατά την τυποποίηση αυτού του επιχειρήματος, οι πράκτορές της εντόπισαν ρητά αντιπαραδείγματα σε μια ιδιότητα κλειστότητας που αυτό χρησιμοποιούσε: μια πράξη που θεωρούνταν ότι διατηρεί τις σχετικές απλές ομάδες μέσα σε μια συγκεκριμένη οικογένεια μπορούσε να παράγει μια ομάδα που αποκλειόταν ρητά από αυτήν.

Σύμφωνα με την περιγραφή της εταιρείας, ξεκινώντας από την PSL₂(49), της οποίας η involution του σώματος έχει κεντροποιητή την PGL₂(7), η πράξη δίνει την απλή συνιστώσα PSL₂(7), η οποία αποκλείεται από την οικογένεια επειδή το 7 είναι πρώτος αριθμός Mersenne. Η Axiom σημειώνει ότι τα αντιπαραδείγματα δεν αναιρούσαν το ίδιο το UGT ούτε καν το συμπέρασμα της Πρότασης II.5.9(ii) του Walter.

Η διόρθωση βασίστηκε στη θεωρία του Solomon του 1976 για τις μέγιστες 2-συνιστώσες, η οποία, σύμφωνα με την Axiom, παρείχε τις βασικές ιδέες για ένα εναλλακτικό επιχείρημα που παρήγαγε και τυποποίησε το σύστημα AxiomProver. Το καθοριστικό βήμα, το οποίο διατυπώνεται στη δημοσίευση ως Θεώρημα 2.3 (διατήρηση των απλών κορυφών), περιγράφεται από την Axiom ως νέο αποτέλεσμα στη θεωρία ομάδων, αποδεδειγμένο από το AxiomProver· σε συνδυασμό με τις αναγωγές των Gilman και Solomon και τα θεωρήματα αναγνώρισης των Foote και Harris, δίνει τη μορφή του UGT για απλές ομάδες που απαιτείται για την ταξινόμηση. Μετά την τυποποίηση, οι μαθηματικοί της Axiom βρήκαν μια συντομότερη απόδειξη με μεθόδους πρώτης γενιάς, καταγεγραμμένη ως Παρατήρηση 9.5, η οποία καταλήγει στο ίδιο συμπέρασμα χωρίς το Θεώρημα 2.3.

Η συγκεκριμένη δημοσίευση, The Unbalanced Group Theorem, με συνεισφορές των Colin Defant και Ken Ono, αναρτήθηκε στον διακομιστή προδημοσιεύσεων Hexagon ως έκδοση 1 στις 27 Οκτωβρίου 2026, με άδεια CC BY 4.0· η σελίδα του έργου αναφέρει ότι έχει 35 σελίδες. Η Axiom αναφέρει ότι συνεργάζεται με θεωρητικούς ομάδων για να συγκεντρώσει τις διορθώσεις που έχουν εντοπιστεί στη βιβλιογραφία και θα τις δημοσιεύσει στη σελίδα διορθώσεων του έργου. Οι Lyons και Solomon, το έργο των οποίων αποτελεί θεμέλιο της ταξινόμησης, συμμετείχαν σε διαβουλεύσεις για τη διόρθωση του UGT, και η εταιρεία δηλώνει ότι θα συνεχίσει να επιμελείται και να επιλύει τις διορθώσεις μαζί με συμβουλευτική επιτροπή στην οποία συμμετέχουν και οι δύο, καθώς και με τον εξωτερικό σύμβουλο Dan Nakano. Η Axiom παρουσιάζει τη συμβολή της ως προσπάθεια να καταστήσει την απόδειξη μηχανικά ελέγξιμη, να τεκμηριώσει τα εμπόδια που συνάντησε και να παράσχει τυποποιημένα επιχειρήματα που τα επιλύουν, διευκρινίζοντας παράλληλα ότι η ταξινόμηση παραμένει επίτευγμα των μαθηματικών που ανακάλυψαν τις ομάδες και ανέπτυξαν τα επιχειρήματα.