Una dimostrazione controversa in matematica, che ha diviso il campo per oltre un decennio, potrebbe finalmente essere risolta da un giudice improbabile: un programma per computer. Il cuore del dibattito ruota attorno al tentativo di Shinichi Mochizuki del 2012 di risolvere la congettura ABC, un problema di lunga data profondamente radicato nella natura fondamentale dei numeri.
La congettura ABC è incentrata su un’equazione apparentemente semplice che coinvolge tre numeri interi: a + b = c. Presuppone regole specifiche che governano il modo in cui i numeri primi che compongono questi numeri interi devono relazionarsi. Risolvere questo problema apparentemente basilare potrebbe sbloccare profonde intuizioni sulla matematica, con un potenziale impatto su altre famose congetture come l’Ultimo Teorema di Fermat.
Mochizuki, professore all’Università di Kyoto in Giappone, ha presentato la sua dimostrazione all’interno di un quadro complesso da lui inventato chiamato teoria interuniversale di Teichmüller (IUT). Tuttavia, il puro tecnicismo e l’oscurità della teoria IUT la resero in gran parte incomprensibile alla maggior parte dei matematici che tentavano di verificare il suo lavoro. L’entusiasmo iniziale lasciò il posto alla frustrazione mentre gli esperti faticavano a decifrarne le complessità.
Aggiungendo benzina sul fuoco, nel 2018, due eminenti matematici tedeschi, Peter Scholze e Jakob Stix, hanno identificato un potenziale difetto nella dimostrazione di Mochizuki. Mochizuki si oppose alla loro tesi e, senza un organismo generale che arbitrasse le controversie matematiche, il campo si divise in due campi: quelli che accettavano ampiamente la visione tradizionale (sostenuta dalla maggior parte dei matematici) e un gruppo più piccolo allineato con Mochizuki e il suo istituto di Kyoto.
Ora, Mochizuki propone un percorso da seguire attraverso la formalizzazione, convertendo la sua dimostrazione da una notazione matematica leggibile dall’uomo a Lean, un linguaggio di programmazione per computer appositamente progettato per una rigorosa verifica matematica. Questo processo potrebbe potenzialmente consentire ai computer di verificare automaticamente la coerenza delle sue argomentazioni, offrendo un livello di obiettività senza precedenti.
Mochizuki ritiene che il Lean sia attrezzato in modo unico per superare i complessi ostacoli linguistici e concettuali che hanno bloccato il progresso nella comprensione della teoria IUT. Lo vede come uno strumento per liberare la verità matematica dai potenziali pregiudizi inerenti all’interpretazione umana.
Sebbene alcuni esperti come Kevin Buzzard dell’Imperial College di Londra considerino questa una direzione promettente, riconoscono anche la sfida colossale che ci attende. Formalizzare la teoria IUT richiederebbe la traduzione di vaste fasce di equazioni complesse nella sintassi Lean, un’impresa simile ad alcuni dei più grandi progetti di formalizzazione mai intrapresi. Tali sforzi spesso coinvolgono team dedicati di matematici e programmatori che durano mesi o addirittura anni.
Johan Commelin dell’Università di Utrecht nei Paesi Bassi, pur essendo cautamente ottimista, sottolinea che il successo dipende dall’impegno costante di Mochizuki. Egli avverte che se il progetto verrà abbandonato prematuramente, potrebbe semplicemente diventare un altro capitolo di una lunga saga segnata da controversie irrisolte.
Anche in caso di successo, Commelin sottolinea che anche con il codice verificato dal computer, i disaccordi sull’interpretazione potrebbero persistere. Il Lean potrebbe risolvere le contraddizioni logiche ma non necessariamente eliminare tutte le differenze filosofiche o concettuali che circondano il lavoro di Mochizuki.
In definitiva, anche se la formalizzazione offre un barlume di speranza per risolvere questo duraturo stallo matematico, resta da vedere se riuscirà a superare le complessità profondamente radicate e le diverse prospettive che hanno caratterizzato il dibattito sulla dimostrazione della congettura ABC.
