L’AI non batte (ancora) gli umani in problemi matematici inediti: i risultati del test “First Proof”

L'intelligenza artificiale è stata battuta dagli umani nella risoluzione di 10 complicati problemi matematici all'interno del progetto "First Proof". Il progetto nasce da questa domanda: l'AI potrà sostituire i matematici? Per provare a rispondere, un gruppo di ricercatori di diverse università europee e statunitensi ha creato il progetto “First Proof”, che significa “prima dimostrazione”. L’obiettivo di questo progetto è valutare la capacità dell'AI nel risolvere problemi matematici complessi, la cui dimostrazione non è mai stata pubblicata prima.

Il team di First Proof, che aveva già organizzato una prima prova meno “ufficiale” a febbraio, ha sottoposto 10 problemi inediti di matematica estremamente avanzata a quattro diversi modelli di AI. Le risposte sono state poi valutate da esperti del settore, proprio come per una normale revisione di una ricerca scientifica. I risultati, pubblicati sul sito di First Proof il 10 giugno, mostrano che, ad ora, l’AI è ancora lontana dal livello dei migliori ricercatori umani. Il sistema più performante, creato dall’Università di Zurigo, è riuscito a dimostrare solo 6 quesiti su 10. Il peggiore, quello dell’Università di Princeton, ne ha dimostrati soltanto 2.

Com’è stato strutturato il test e qual è lo scopo

Valutare le effettive capacità matematiche dell'AI non è semplice. Uno dei problemi principali è che i modelli vengono allenati su enormi quantità di testi, articoli scientifici e materiale disponibile online. Se un quesito è troppo simile a qualcosa già presente nei dati di allenamento, il rischio è che il sistema riesca a risolverlo semplicemente riproponendo una soluzione già presente nei dati su cui è stato allenato, sembrando più capace di quanto non sia.

Per riuscire a testarne davvero le capacità, il team di “First Proof” ha chiesto a ricercatori di tutto il mondo di inviare problemi, quesiti e teoremi che avevano risolto nel corso delle proprie ricerche, ma che non avevano ancora pubblicato né in articoli scientifici né online. Tra tutte le proposte ne sono state selezionate dieci, appartenenti a diverse branche della matematica, dalla geometria all'algebra fino alla probabilità.

I sistemi di intelligenza artificiale hanno dovuto affrontare questi problemi in modo completamente autonomo, senza assistenza umana. Le soluzioni sono state poi esaminate da un gruppo di circa trenta matematici, seguendo un processo simile a quello utilizzato nella revisione degli articoli scientifici.

Sono state testate quattro AI diverse e ha vinto l’ETH di Zurigo

Alla sfida hanno preso parte quattro modelli di AI. L'unica grande azienda presente direttamente è stata OpenAI con ChatGPT 5.5 Pro. Gli altri tre sistemi sono stati sviluppati da gruppi di ricerca dell'Università della California di Los Angeles (UCLA), della Princeton University del New Jersey e del Politecnico Federale (ETH) di Zurigo.

Tutte e tre le università hanno sviluppato dei cosiddetti “harness”, cioè sistemi di AI in un cui un modello (ad esempio ChatGPT) produce una soluzione e altri modelli (ad esempio Gemini e Claude) la controllano, la criticano e la migliorano attraverso una serie di passaggi successivi. Il sistema vincitore dell'ETH di Zurigo funzionava proprio così: ChatGPT generava una possibile dimostrazione, che veniva poi verificata e migliorata con il contributo di Gemini e Claude.

Come dicevamo, l'harness dell’ETH di Zurigo è stato il migliore, risolvendo e dimostrando correttamente 6 problemi su 10. Al secondo posto si è classificato il team UCLA, seguito da ChatGPT 5.5 Pro. Ultimo il sistema di Princeton, che, con un harness basato principalmente su Gemini 3.1 Pro, è riuscito a dimostrare solamente due quesiti.

Tutto questo, però, non è stato senza costi. I sistemi creati dalle tre università, proprio per i loro meccanismi di verifica continua, erano incredibilmente dispendiosi. Il modello dell’ETH è arrivato a consumare 950 dollari nel tentativo di risolvere un singolo problema, senza riuscirci. Per confronto, ChatGPT 5.5 Pro utilizzato da solo ha richiesto solo 144 dollari per affrontare l'intero set di dieci problemi.

Perché l'AI non può ancora sostituire i matematici

Dopo la competizione, il team di First Proof ha cercato di capire perché alcuni dei problemi proposti fossero rimasti irrisolti. La conclusione principale è che questi quesiti richiedevano idee o strategie molto diverse da quelle presenti nella letteratura matematica esistente. Secondo Johannes Schmitt, membro del team dell'ETH di Zurigo, spesso all'AI mancava proprio "un'idea critica e inaspettata", quel passaggio creativo necessario per completare il ragionamento e arrivare alla dimostrazione.

Un altro limite emerso riguarda il modo in cui i modelli costruiscono le dimostrazioni. Le AI tendevano a sviluppare con grande precisione le parti più procedurali e meccaniche, quelle considerate più noiose dagli umani, ma, nei passaggi più concettualmente complessi tendevano a essere molto meno rigorose. In alcuni casi davano per scontati risultati che avrebbero richiesto una dimostrazione, senza fornire alcuna giustificazione. In altri citavano articoli che in realtà non contenevano il risultato menzionato.

Questo non significa che l'intelligenza artificiale sia inutile per la ricerca matematica. Al contrario, il test mostra che può già essere uno strumento utile per verificare passaggi e farsi supportare nelle dimostrazioni. Il team di First Proof inizierà ad agosto a preparare una nuova edizione del test, prevista per ottobre 2026. Secondo gli organizzatori, le prossime versioni del test potrebbero aiutare a capire meglio in quali contesti l'intelligenza artificiale possa diventare davvero utile ai matematici, dalla verifica delle dimostrazioni alla ricerca di nuove strategie per affrontare problemi ancora aperti.

non perderti questo articolo

ChatGPT ha risolto in 80 minuti un problema matematico irrisolto dal 1966