Δύο ομάδες μαθηματικών προσπαθούν να βάλουν το Lean στην καρδιά της διαμάχης για την υπόθεση ABC. Η μία δουλεύει μυστικά πάνω από δύο χρόνια, ενώ η άλλη έχει ήδη πιάσει το πιο δύσκολο σημείο της απόδειξης.
Δύο ομάδες μαθηματικών έχουν ξεκινήσει να τυποποιούν σε πρόγραμμα του υπολογιστή την αμφιλεγόμενη απόδειξη της υπόθεσης ABC, σε μια προσπάθεια που μπορεί να ξεμπλοκάρει μία από τις πιο σκληρές διαμάχες των σύγχρονων μαθηματικών. Η μία ομάδα λειτουργούσε μυστικά για περισσότερα από δύο χρόνια, πριν γίνει γνωστή η δουλειά της, ενώ η άλλη έχει ήδη ανοίξει δημόσια τον ίδιο δρόμο, με τον Σινίτσι Μοχίζουκι στο επίκεντρο.
Η ιστορία ξεκινά το 2012, όταν ο Μοχίζουκι, από το Πανεπιστήμιο του Κιότο, δημοσίευσε διαδικτυακά μια απόδειξη 500 σελίδων για την υπόθεση ABC στη θεωρία αριθμών. Η πρόταση ακούγεται απλή: αφορά τους πρώτους αριθμούς που εμφανίζονται σε λύσεις της εξίσωσης a + b = c και τον τρόπο που σχετίζονται μεταξύ τους. Η απόδειξη όμως στηρίζεται σε βαθιές ιδέες για το πώς αλληλεπιδρούν η πρόσθεση και ο πολλαπλασιασμός, με συνέπειες που αγγίζουν και άλλους κλάδους των μαθηματικών.
Το πρόβλημα δεν ήταν μόνο η πολυπλοκότητα. Ο Μοχίζουκι έφερε μαζί του μια σειρά από νέες έννοιες και τεχνικές, που ονόμασε Inter-universal Teichmüller theory, ή IUT. Πολλοί κορυφαίοι μαθηματικοί προσπάθησαν να διαβάσουν, να ελέγξουν και να συζητήσουν την εργασία του, ακόμη και μαζί του, αλλά η συζήτηση κόλλησε. Το 2018, όταν οι Πίτερ Σολτσε και Γιάκομπ Στιξ ανακοίνωσαν ότι εντόπισαν πιθανό σφάλμα, η αντιπαράθεση πάγωσε ακόμη περισσότερο. Ο Μοχίζουκι και οι στενοί συνεργάτες του επέμεναν ότι η απόδειξη είναι σωστή, ενώ μεγάλο μέρος της κοινότητας τη θεωρούσε είτε ακατανόητη είτε λανθασμένη.
Την περασμένη χρονιά, όμως, άνοιξε μια νέα διέξοδος. Η τυποποίηση μαθηματικών αποδείξεων έχει προχωρήσει αρκετά, μετατρέποντας τις γραπτές αποδείξεις σε γλώσσα που μπορεί να ελέγχει αυτόματα ένας υπολογιστής. Το Lean, ένα από τα πιο εξελιγμένα τέτοια συστήματα, έγινε το βασικό εργαλείο. Στα τέλη του 2023 ο Φουμιχάρου Κάτο, από το ZEN Mathematics Center στην Ιαπωνία, ξεκίνησε το LANA, συγκεντρώνοντας ερευνητές που γνωρίζουν τη δουλειά του Μοχίζουκι και ειδικούς στο Lean που έχουν ήδη τυποποιήσει μεγάλα μαθηματικά έργα. Στόχος, όπως είπε ο Άνταμ Τοπάζ από το Πανεπιστήμιο της Αλμπέρτα, ήταν να κλείσει η διαμάχη «μια για πάντα».
Το LANA όμως έφτασε στο ίδιο ακριβώς σημείο όπου είχε σταματήσει η συζήτηση για το 2018. Ο Κάτο μίλησε για «βαθιά κατανόηση» της ιδέας του Μοχίζουκι, αλλά και για ένα συγκεκριμένο σημείο στην IUT που δεν μπορούσαν να ξεπεράσουν. «Έχουμε ουσιαστικά κολλήσει στην προσπάθεια να καταλάβουμε αυτό το σημείο», είπε ο Τοπάζ. Παράλληλα, ο ίδιος ο Μοχίζουκι και οι συνεργάτες του ξεκίνησαν δικό τους εγχείρημα τυποποίησης στο Lean, όχι τόσο για να αποδείξουν εκ νέου ότι η εργασία του είναι σωστή, όσο για να την αποσαφηνίσουν με ακρίβεια. Σε πρόσφατη ομιλία του στο Πανεπιστήμιο του Έξετερ, εξήγησε ότι το Lean μπορεί να λειτουργήσει σαν ακριβές αρχείο της λογικής δομής της IUT, απαλλαγμένο από παρερμηνείες.
Ο Μοχίζουκι λέει ότι η ομάδα του έχει ήδη γράψει 70 γραμμές κώδικα στο Lean, ξεκινώντας από το πιο αμφισβητούμενο τμήμα της απόδειξης και προχωρώντας σε ένα σχέδιο τεσσάρων επιπλέον σταδίων. Ο Κέβιν Μπάζαρντ, από το Imperial College London, επισημαίνει ότι αυτό είναι ελάχιστο για το μέγεθος του εγχειρήματος. «Με 70 γραμμές παλεύεις να αποδείξεις δυο θεωρήματα προπτυχιακού επιπέδου, όχι μια γιγάντια απόδειξη», είπε. Παρ’ όλα αυτά, η κινητικότητα γύρω από το Lean έχει αλλάξει το κλίμα: για πρώτη φορά εδώ και χρόνια, η συζήτηση δεν περιστρέφεται μόνο γύρω από αδιέξοδα, αλλά γύρω από έναν ζωντανό, έστω και δύσκολο, διάλογο μεταξύ των δύο πλευρών.
