Μια γλώσσα προγραμματισμού, σχεδιασμένη για την αξιόπιστη επαλήθευση μαθηματικών θεωρημάτων και τον εντοπισμό λογικών σφαλμάτων, χρησιμοποιήθηκε για την ανάλυση μιας εργασίας φυσικής – και εντόπισε ένα σφάλμα.
Η ανακάλυψη αυτή εγείρει ερωτήματα σχετικά με το πόσες άλλες εργασίες ενδέχεται να περιέχουν παρόμοια προβλήματα
Το εξειδικευμένο λογισμικό χρησιμοποιείται όλο και περισσότερο για να βοηθήσει τους μαθηματικούς να ελέγξουν ότι οι αποδείξεις τους είναι σωστές και απαλλαγμένες από αντιφάσεις και λογικά κενά, χρησιμοποιώντας μια διαδικασία γνωστή ως τυποποίηση.
Η προσέγγιση αυτή έχει μάλιστα προταθεί ως πιθανή λύση σε μερικά από τα πιο δύσκολα προβλήματα των μαθηματικών, όπως η εκτενής, 500 σελίδων απόδειξη του Σινίτσι Μοτσιζούκι για την υπόθεση ABC, για την οποία οι ειδικοί διαφωνούν εδώ και χρόνια.
Τώρα, ο Τζόζεφ Τούμπι Σμιθ από το Πανεπιστήμιο του Μπαθ, στο Ηνωμένο Βασίλειο, εφάρμοσε μια γλώσσα τυποποίησης που ονομάζεται Lean στον τομέα της φυσικής.
Προσπάθησε να τυποποιήσει μια έρευνα που δημοσιεύθηκε το 2006 σχετικά με τη σταθερότητα του δυναμικού του μοντέλου των δύο διπλών Higgs (2HDM), η οποία έχει αναφερθεί ευρέως τα τελευταία χρόνια, αλλά κατά λάθος αποκάλυψε ένα σφάλμα που υπονομεύει το θεώρημα.
Το σφάλμα σχετίζεται με μια δήλωση στην οποία οι αρχικοί συγγραφείς λένε ότι μια συγκεκριμένη συνθήκη, C, είναι επαρκής για μια σταθερή λύση στο πρόβλημα. Αλλά ο Tooby-Smith έδειξε κατά τη διάρκεια της επισημοποίησης ότι υπάρχει μια συνθήκη C που δεν παρέχει σταθερή λύση.
Ο Τούμπι Σμιθ αναφέρει ότι η ανακάλυψη του σφάλματος έχει δραματική επίδραση στην ίδια την εργασία, αλλά είναι απίθανο να προκαλέσει προβλήματα σε μεταγενέστερες εργασίες που βασίστηκαν σε αυτήν και την ανέφεραν.
Ωστόσο, φοβάται πλέον ότι πολλές εργασίες φυσικής περιέχουν παρόμοια λάθη, χωρίς όμως να είναι σίγουρος για το πόσο εκτεταμένο μπορεί να είναι το πρόβλημα. Θεωρεί ότι αυτό αποτελεί ισχυρό επιχείρημα υπέρ της καθιέρωσης της τυποποίησης ως βασικού στοιχείου της δημοσίευσης νέων ερευνητικών εργασιών.
Ο Τούμπι Σμιθ λέει ότι οι φυσικοί τείνουν να μην δίνουν τόσες σαφείς λεπτομέρειες στα θεωρήματα όσο οι μαθηματικοί. «Επειδή πολλοί φυσικοί δεν ενδιαφέρονται για αυτές τις λεπτές λεπτομέρειες, μερικές φορές τις χάνουν και εκεί είναι που γίνεται ένα λάθος», λέει.
Ο Κέβιν Μπάζαρντ του Imperial College του Λονδίνου αναφέρει ότι η τυποποίηση έχει μεγάλη επίδραση στα μαθηματικά και ότι δεν υπάρχει λόγος για τον οποίο η θεωρητική φυσική, τουλάχιστον, να μην μπορεί να αντιμετωπιστεί με τον ίδιο τρόπο. «Προσπαθήσαμε να εφαρμόσουμε αυτή την προσέγγιση στα μαθηματικά και αποδείχθηκε πραγματικά ενδιαφέρουσα», λέει.
Αλλά το πραγματικό όφελος της τυποποίησης στα μαθηματικά προέρχεται τώρα από το μεγάλο σώμα των υπαρχόντων τυποποιημένων θεωρημάτων, το οποίο επιτρέπει στους μαθηματικούς να χτίζουν πιο εύκολα πάνω σε αυτά και επίσης να εκπαιδεύουν μοντέλα τεχνητής νοημοσύνης που μπορούν να βοηθήσουν στην ταχύτερη τυποποίηση νέων θεωρημάτων.
Η εκπαίδευση αυτή ωστόσο χρειάστηκε χρόνο και πολλά συγκεκριμένα παραδείγματα για να χρησιμοποιηθούν ως δεδομένα εκπαίδευσης, τα οποία μπορεί να μην είναι ακόμη διαθέσιμα για τη φυσική.
«Στην ιδανική περίπτωση, χρειαζόμαστε ένα εκατομμύριο γραμμές φυσικής, και αυτό μπορεί να είναι σκληρή δουλειά για να το αποκτήσουμε. Εάν οι μηχανές δεν είναι αρκετά καλές στο να κάνουν φυσική αρχικά, τότε θα υπάρξει χειρωνακτική εργασία στην αρχή και στη συνέχεια τελικά οι μηχανές ελπίζουμε να αναλάβουν», λέει ο Μπάζαρντ .
