Il benchmark First Proof è stato progettato per verificare una capacità molto diversa da quella misurata nei tradizionali test matematici per modelli linguistici. Non propone esercizi scolastici, quesiti olimpici o problemi già presenti in archivi e pubblicazioni, ma dieci questioni di ricerca provenienti dal lavoro reale di matematiche e matematici attivi in discipline differenti. Le soluzioni erano note agli autori dei problemi, ma non erano state pubblicate né rese disponibili online, riducendo il rischio che un sistema potesse riprodurre materiale già incontrato durante l’addestramento.
La seconda edizione del test, svolta tra marzo e giugno 2026, ha trasformato il primo esperimento informale in una valutazione strutturata. I problemi dovevano richiedere un’intuizione non standard e avere una dimostrazione umana nota di lunghezza non superiore a otto pagine. I quattro sistemi testati hanno ricevuto gli stessi dieci quesiti in formato LaTeX, hanno lavorato senza ulteriori interazioni con gli organizzatori e hanno dovuto produrre le proprie dimostrazioni entro ventiquattro ore. Le risposte sono state poi esaminate da almeno due revisori specialisti per ciascun problema, con una classificazione che distingueva tra risultati sostanzialmente corretti, risultati da correggere in modo marginale, risultati che richiedevano revisioni importanti e tentativi respinti.
Il sistema con il risultato migliore ha ottenuto sei soluzioni accettate su dieci. Si trattava di un harness sviluppato da un gruppo accademico dell’ETH di Zurigo e dell’Università di Aarhus, costruito per far generare una risposta iniziale a ChatGPT e sottoporla poi a controlli e revisioni tramite un insieme di modelli diversi. Alle sue spalle si sono collocati un sistema sviluppato dall’UCLA, ChatGPT 5.5 Pro utilizzato direttamente da OpenAI e un harness di Princeton basato soprattutto su Gemini 3.1 Pro. Il dato mostra che l’orchestrazione di più modelli, con fasi dedicate a critica, verifica e riscrittura, può migliorare il risultato rispetto a una singola generazione, ma anche che questo miglioramento richiede infrastrutture, procedure e costi molto più elevati.
Nel complesso, sette dei dieci problemi hanno ricevuto almeno una soluzione giudicata corretta o correggibile con interventi minori. Un caso particolarmente significativo ha riguardato un problema di equazioni differenziali stocastiche, risolto correttamente con un approccio nuovo e differente dalla soluzione prodotta dagli autori umani. In altri casi, i modelli hanno individuato argomentazioni originali, soprattutto nei problemi di combinatoria, analisi stocastica e algebra. Questo non significa però che abbiano dimostrato una competenza uniforme nella matematica di ricerca: un problema di geometria metrica non ha prodotto alcun progresso sostanziale da parte di nessuno dei quattro sistemi.
Il limite più evidente non è stato soltanto la mancata soluzione di alcuni quesiti, ma il modo in cui i modelli gestivano le parti più difficili di una dimostrazione. Le risposte tendevano a sviluppare con precisione passaggi di routine e a dedicare molto spazio a calcoli secondari, mentre proprio nei punti in cui serviva un’intuizione nuova o una giustificazione rigorosa comparivano salti logici, richiami generici a “argomenti standard” e affermazioni non dimostrate. I revisori hanno inoltre rilevato citazioni inesatte, riferimenti bibliografici che non contenevano realmente il risultato dichiarato e casi in cui i sistemi riutilizzavano terminologia, struttura e persino formulazioni di lavori precedenti senza citarli.
Il benchmark evidenzia quindi una distinzione importante tra la capacità di generare una dimostrazione plausibile e la capacità di produrre una prova effettivamente valida. In matematica avanzata, una risposta può apparire formalmente sofisticata, utilizzare notazioni corrette e seguire una strategia credibile, ma fallire in un singolo passaggio decisivo. La verifica non può essere affidata alla sola coerenza stilistica dell’output: richiede revisione specialistica, controllo delle fonti, valutazione delle ipotesi utilizzate e analisi della continuità logica dell’intera argomentazione.
First Proof misura soltanto la fase di soluzione di problemi già formulati e non valuta ancora aspetti centrali della ricerca matematica, come la capacità di proporre nuove congetture interessanti, definire concetti utili o costruire nuovi quadri teorici. Il risultato più rilevante non è quindi che l’AI non riesca ancora a sostituire le migliori competenze umane, ma che possa già contribuire in alcuni contesti alla ricerca esplorativa, soprattutto quando opera come strumento sottoposto a controllo umano rigoroso. L’uso più concreto non è l’autonomia completa del modello, ma l’integrazione in flussi di lavoro dove l’AI produce tentativi, confronta strategie, sviluppa casi particolari e accelera la fase iniziale, mentre la validazione resta affidata a matematici in grado di individuare errori, lacune e collegamenti realmente nuovi.