Η Axiom Math δημοσίευσε πλήρη τυποποίηση στη γλώσσα αποδείξεων Lean της ταξινόμησης των πεπερασμένων απλών ομάδων, ενός από τα μεγαλύτερα θεωρήματα των μαθηματικών. Το έργο ακολουθεί την απόδειξη της πρώτης γενιάς, που είναι διάσπαρτη σε εκατοντάδες εργασίες, και φτάνει τα 43,1 εκατ. γραμμές κώδικα Lean με 2,05 εκατ. δηλώσεις. Κάθε λογικό βήμα ελέγχθηκε από τον πυρήνα της Lean. Η ομάδα αναφέρει ότι εντόπισε και διόρθωσε 34 αποκλίσεις από δημοσιευμένα επιχειρήματα, ανάμεσά τους ένα πρόβλημα στο λεγόμενο Unbalanced Group Theorem.

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

Διαβάστε το πρωτότυπο στο Axiom Math

Σχετική υπηρεσία: Ανάπτυξη λογισμικού

Σχετικές ειδήσεις