Una prova corretta può diventare troppo lunga per essere capita

Un’AI produce una dimostrazione, un programma la controlla, il risultato è corretto. Poi qualcuno deve ancora capire che cosa è successo. Nel saggio ospitato da Terence Tao, il matematico Francesco Maggi parte da questa distanza per immaginare due futuri della ricerca.

In quello luminoso, ottenere prove più facilmente libera spazio per nuove idee. In quello buio, i risultati aumentano mentre si indeboliscono le persone e le comunità capaci di interpretarli. Il buio può quindi essere pieno di pubblicazioni.

Le lunghissime prove formali sono un caso concreto: verificarne i passaggi non basta a ricavarne una spiegazione leggibile o un’intuizione da usare altrove. Maggi vede ancora molto lavoro per i matematici, proprio dentro quella distanza tra aver ottenuto un risultato e riuscire a farci qualcosa.