DeepMind risolve nove problemi matematici aperti con AlphaProof Nexus
Google DeepMind ha annunciato che il suo sistema AlphaProof Nexus ha risolto da solo nove problemi matematici rimasti aperti, due dei quali resistevano da 56 anni. Il lavoro è stato pubblicato sulla rivista Science dopo la revisione dei pari.
- AlphaProof Nexus ha risolto 9 problemi di Erdos aperti, due da 56 anni.
- Le dimostrazioni sono scritte in Lean e controllate passo per passo dal computer.
- Lo studio è passato dalla revisione dei pari su Science, a differenza dei risultati OpenAI pubblicati su GitHub.
Che cosa ha risolto il sistema
I nove problemi fanno parte di una raccolta di 353 questioni aperte legate al matematico Paul Erdős. Oltre a questi, secondo quanto riportato nello studio, AlphaProof Nexus ha dimostrato 44 congetture tratte dal database OEIS delle sequenze di numeri interi, ha risolto una questione aperta di geometria algebrica e ha migliorato un limite noto nell'ottimizzazione min-max, una tecnica usata anche per addestrare alcuni modelli di IA.
Il sistema è costruito attorno a Gemini 3.1 Pro, il modello di Google, che scrive e corregge le dimostrazioni. Per i passaggi più difficili può appoggiarsi ad AlphaProof, uno strumento specializzato. Google DeepMind riferisce che anche senza quell'aiuto i nove problemi di Erdős sono stati risolti. Le soluzioni erano state condivise online prima della pubblicazione dell'articolo scientifico.
Il nodo della verifica formale
La differenza rispetto ad altri annunci sta nel modo in cui i risultati vengono controllati. Le dimostrazioni sono scritte in Lean, un linguaggio formale: ogni passaggio viene verificato dal computer, che segnala subito l'errore. I messaggi di errore guidano il tentativo successivo, in un ciclo di correzione automatica. Un modello linguistico, da solo, può produrre argomentazioni convincenti ma sbagliate; in Lean questo non passa inosservato.
Al controllo automatico si è aggiunta la revisione dei pari di una rivista scientifica, cioè la valutazione da parte di altri matematici prima della pubblicazione. Lo studio arriva in un momento di tensione: OpenAI ha pubblicato centinaia di dimostrazioni prodotte dalla sua IA direttamente su GitHub, senza sottoporle a una rivista, e l'Association for Human Mathematics, guidata da Terence Tao, ha invitato al boicottaggio.
Perché conta
La matematica è uno dei campi in cui è più facile capire se un sistema di IA ha davvero ragione oppure no: o la dimostrazione regge, o non regge. Per questo è diventata il terreno di prova principale per misurare i progressi reali dei modelli, al di là degli annunci.
La vicenda mostra anche due strade diverse per presentare i risultati: pubblicare subito online, oppure passare dal doppio filtro della verifica formale e della revisione umana. La seconda è più lenta, ma rende i risultati controllabili da chiunque. È una distinzione che riguarda anche settori ben oltre la matematica, dalla ricerca scientifica alla sicurezza informatica, dove sapere se l'output di un modello è verificato o solo plausibile fa tutta la differenza.
