Un paio di settimane fa, nella mia rubrica su MaddMaths! (come? non la leggete? male!), scrissi che il progetto First Proof aveva preparato dieci lemmi mai pubblicati da dimostrare in una settimana, e che gli LLM erano riusciti a farcela solo in due casi. A quanto pare questo era il risultato che gli ideatori della gara erano riusciti a fare con le versioni “ufficiali” dei programmi. In realtà sia OpenAI che Google con il suo Aletheia dicono di aver risolto cinque (o sei, se si accetta una dimostrazione incompleta) problemi. E la cosa più interessante è che non sono gli stessi: insieme i due software hanno dimostrato otto dei dieci lemmi.

Come riporta Scientific American, non è chiaro se questi risultati dipendano dal fatto che internamente queste aziende hanno modelli più avanzati di quelli pubblicamente disponibili, oppure c’è stato un qualche aiutino da parte di matematici umani, anche se Google lo ha decisamente negato. La domanda non è affatto peregrina. Penso che ormai sia sdoganato il fatto che un’IA riesca a fare almeno in parte il lavoro di un dottorando – sì, devo ancora studiarmi i cicli di Claude che sono piaciuti così tanto a Knuth – anche sfruttando la loro capacità di trovare nella vastissima letteratura idee simili da portare avanti. In fin dei conti è ben noto questo racconto di Julia Robinson: “Lunedì – cercato di dimostrare teorema. Martedì – cercato di dimostrare teorema. Mercoledì – cercato di dimostrare teorema. Giovedì – cercato di dimostrare teorema. Venerdì – il teorema è falso”. Traduciamolo nel mondo degli LLM: essi possono produrre centinaia di “dimostrazioni” che si scopre poi essere false, perché assumono ipotesi non necessariamente vere. I sistemi di verifica automatica buttano via queste dimostrazioni errate e l’IA non si abbatte e ricomincia; diciamo però che se un essere umano vede quello che potrebbe essere un approccio interessante e spinge il sistema in quella direzione è molto più facile arrivare al risultato finale.

Per ovviare a questo problema, il gruppo dietro First Proof sta preparando una seconda gara, ma questa volta chiederà di poter far girare lui stesso i programmi, per essere certi che non ci sia aiuto esterno. Vedremo (a) se i produttori di questi sistemi accetteranno e (b) che succederà.

Ultimo aggiornamento: 2026-03-18 16:46