Problemi del millennio, la sfida tra matematici e AI è aperta

Ieri è stata data la notizia della risoluzione di uno dei sette famosi problemi "del Millennio", definiti nel 2000 dal Clay Institute come reiterazione dei 23 problemi proposti nel 1900 dal famoso matematico tedesco David Hilbert, per caratterizzare la matematica del XX secolo.

Il problema risolto (Esistenza e regolarità per l'equazione di Navier-Stokes), consiste nel comprendere le proprietà di regolarità delle soluzioni di una equazione fondamentale che modellizza moti di fluidi (aria, acqua, sangue,...).

Dei sette problemi ne era stato finora risolto solo uno: la congettura di Poincaré, nel 2002 dal matematico russo Grigorij Perel’man.

Ma il punto è che l'autore della dimostrazione non è un matematico o un gruppo di matematici in carne e ossa, ma un modello di intelligenza artificiale.

L'annuncio è stato dato ieri, 8 settembre, da "OpenAI", nota per l'assistente basato sull'intelligenza artificiale "ChatGPT".

La notizia è stata un vero e proprio fulmine a ciel sereno. Si sapeva che l'IA stesse facendo progressi anche in ambito matematico, ma qui si tratta di un problema di primissimo livello, su cui stavano lavorando, da decenni, schiere di matematici anche incentivati da una non trascurabile ricompensa: alla risoluzione dei problemi del Millennio viene corrisposto infatti un premio in denaro di un milione di dollari.

Al di là delle polemiche che inevitabilmente stanno dilagando riguardo alla paternità della soluzione, è naturale chiedersi cosa stia succedendo: un’attività, considerata l’apice del raziocinio umano, è ora preda di agenti software che affrontano e risolvono problemi di punta parlando tra loro. L’uomo di scienza assume il ruolo di copilota suggerendo ad un LLM (Large Language Model) di cosa occuparsi e indicando magari alcune fonti bibliografiche.

Qual è ora il rapporto tra un matematico e le intelligenze artificiali? Cosa accadrà nel prossimo futuro?

Ad un famoso matematico è stato chiesto quale fosse la prima cosa che avrebbe voluto sapere al risveglio, dopo un periodo di ibernazione di cento anni; la sua risposta fu: “E’ stata dimostrata l’ipotesi di Riemann?”.  Si tratta di un altro dei sette Problemi del Millennio, l’unico che era già presente tra i 23 problemi di Hilbert, rimasto tuttora irrisolto da ben più di un secolo.

La dimostrazione comunicata da OpenAI è stata anche formalizzata, cioè garantita esente da errori, con un codice LEAN lungo 13 milioni di righe, apparentemente al di là della possibilità di comprensione umana. Ciò mette fortemente in discussione l’idea stessa di dimostrazione e tutto il processo che porta ad un risultato matematico, con i suoi errori, aggiustamenti e non da ultimo, il consenso della comunità scientifica.