Un sistema di ricerca basato sull'intelligenza artificiale è riuscito a dimostrare la congettura di Aaronson-Ambainis, un problema matematico rimasto aperto per ben 18 anni. La notizia ha dell'incredibile: ciò che per anni ha resistito ai tentativi dei matematici è stato risolto in appena tre giorni da un'IA sviluppata da PSI, un risultato che segna un punto di svolta nel rapporto tra intelligenza artificiale e ricerca matematica.
Una sfida lunga quasi due decenni
La congettura di Aaronson-Ambainis, formulata nel 2008, riguarda i limiti dei vantaggi dei computer quantistici: in sostanza, stabilisce quando e quanto i calcolatori quantistici possono essere realmente più potenti dei computer classici. Si tratta di una questione teorica fondamentale, che tocca le fondamenta stesse dell'informatica quantistica e che per anni ha rappresentato un ostacolo insormontabile per i ricercatori.
La verifica formale con Lean
Il punto di forza di questa dimostrazione è la sua verificabilità: ogni passaggio è stato controllato formalmente con Lean, un software in grado di validare in modo rigoroso ogni singolo passo matematico, eliminando il rischio di errori nascosti. Questo aspetto è cruciale, perché garantisce che il risultato non sia frutto di un'illusione o di un ragionamento approssimativo dell'IA, ma di una catena logica solida e certificata.
L'episodio dimostra come l'intelligenza artificiale possa diventare uno strumento concreto al servizio della matematica avanzata, accelerando scoperte che altrimenti richiederebbero anni di lavoro umano. Se da un lato resta aperta la questione su quanto questi sistemi possano essere generalizzati, dall'altro il caso PSI segna un precedente destinato a far discutere: la ricerca matematica del futuro potrebbe essere sempre più un lavoro di collaborazione tra menti umane e algoritmi.
