Maurizio Codogno, meglio noto in rete come .mau., racconta come lui vede la matematica, con la scusa di non doverla insegnare né crearne di nuova. Abbiamo letto tanti titoloni su come le IA sarebbero ormai in grado di risolvere i problemi matematici che hanno tormentato generazioni di matematici. La realtà è un po’ diversa: la creatività non c’è ancora.

Insomma, queste IA sono capaci o no di fare matematica? A gennaio c’è stato l’annuncio su X di un problema di Erdős risolto dall’IA. I problemi di Erdős, come avevo raccontato un paio di mesi fa, sono un migliaio di congetture di teoria dei numeri proposte negli anni da Paul Erdős e raccolte in un sito. In questo caso, la congettura è stata dimostrata falsa, e c’è anche una dimostrazione della sua correttezza usando Lean, un software che permette appunto di verificare automaticamente la correttezza formale dei passaggi. Abbiamo anche avuto un altro caso, ricapitolato qui da Terence Tao e raccontato più ampiamente nel sito dei problemi di Erdős. Insomma, ci siamo? La ricerca matematica sarà ormai appannaggio delle IA? Mah, calmiamoci.

Certo, ci sono stati alcuni altri problemi “risolti” dalle IA, come raccontavo: ma come MaddMaths! ha già raccontato, in quasi tutti i casi il problema era già stato risolto, solo che il gestore del sito non lo sapeva. Diciamolo in un altro modo: le IA sono molto brave a trovare materiale in rete – d’altra parte, come si fa sennò ad addestrarle? – e sputarlo fuori come risposta alla domanda. E il mondo produce così tanta matematica che non è umanamente possibile anche solo conoscere tutti i risultati, non dico comprenderli: e qui il vantaggio competitivo delle IA è indubbio.

Per esempio, come potete leggere in questo articolo, il problema numero 1089 era stato risolto nel 1981 in una nota a un articolo che di Erdős non parlava neppure… Banalmente, qualcun altro aveva avuto la stessa idea del grande matematico – il che non è così strano, mica enunciava proprietà a caso – e aveva trovato la risposta. Ma la cosa peggiore è che questi sistemi producono una quantità enorme di “dimostrazioni” spesso sottilmente erronee, e non siamo ancora arrivati a riuscire a verificarle tutte automaticamente in un tempo finito. Insomma, è come cercare un ago in un pagliaio tirando su casualmente una manciata di paglia e dovendo cercare al suo interno se per caso l’ago ci fosse davvero: in caso contrario si ributta la paglia nel pagliaio e si prende un’altra manciata.

Il 2026 cambierà la situazione? Sappiamo che è difficile fare previsioni sul futuro, ma non credo che con le architetture correnti otterremo un miglioramento un po’ più che marginale. Il vero stato dell’arte è quello testato da First Proof: alcuni matematici hanno compilato un elenco di dieci lemmi che hanno dovuto dimostrare nelle loro ricerche, dando una settimana di tempo a chiunque (senza aiuto umano…) per risolverli. Nei loro test interni, hanno trovato che i sistemi ufficiali erano riusciti a risolvere gli ultimi due problemi, ma la dimostrazione di uno di essi era già stata pubblicata; e non sono riusciti nemmeno a risolvere il primo problema, che pure era fondamentalmente presente in rete.

Il fatto che non ci siano stati altri commenti se non voci senza ulteriore conferme mi fa pensare che in effetti quello sia effettivamente lo stato dell’arte: da soli gli attuali LLM non vanno avanti, e hanno bisogno di una costante interazione con gli umani. Penso che Erdős avrebbe apprezzato, e avrebbe detto che la sua mente era aperta: ma appunto abbiamo bisogno di creativi come lui. A metà marzo ci dovrebbe essere un nuovo round di First Proof: vediamo se ci saranno miglioramenti.

Il tutto tra l’altro non tiene conto che la matematica attuale se evolve anche come creatività: Daniel Litt nota come negli ultimi cinquant’anni siano stati definiti molti nuovi concetti, e Mohammed Abouzaid della Stanford University, capo informale del progetto First Proof, ha notato come la matematica usata dagli LLM sembra quella del diciannovesimo secolo. Ciò non sarebbe nulla di male – la matematica non ha una scadenza, e se qualcuno dimostrasse l’ultimo teorema di Fermat usando solo le tecniche allora conosciute sarebbe un risultatone! – ma non porterebbe avanti le frontiere della matematica. I matematici (quelli veri, non certo io che però tanto sono anzyano con la ipsilon e quindi fuori categoria) possono insomma stare ancora tranquilli.

Guarda la pagina di questa rubrica

Maurizio Codogno

Maurizio Codogno, noto online come .mau., è nato a Torino nel 1963, e si è laureato in matematica presso la Scuola Normale Superiore di Pisa e successivamente in informatica a Torino. Autore di numerosi libri di divulgazione scientifica, tra cui “Matematica in pausa caffè” e “Chiamatemi Pi Greco”, ha il suo blog “Notiziole di .mau.” dall’inizio del millennio ed è stato curatore della collana di libri Matematica di Gazzetta dello Sport e Corriere della Sera.