Lo studio su AlphaProof Nexus, il framework di Google DeepMind per la ricerca di dimostrazioni formali, è stato pubblicato l’8 ottobre 2026. Riporta 9 problemi di Erdős risolti su 353 formalizzati e 44 congetture dell’Online Encyclopedia of Integer Sequences (OEIS) dimostrate su 492 selezionate. Due dei nove problemi di Erdős erano aperti da 56 anni.
Che cosa fa AlphaProof Nexus
AlphaProof Nexus combina modelli linguistici e Lean, un assistente per le dimostrazioni formali: un sistema che controlla matematicamente una prova scritta in un linguaggio rigoroso. Il framework lavora su un teorema già formalizzato e su uno schema di dimostrazione da completare; può ricevere anche contesto in linguaggio naturale e conoscenze di dominio codificate in Lean.
Questo punto definisce il compito: il sistema cerca una dimostrazione per un enunciato espresso formalmente. Il processo descritto nello studio non parte da una domanda matematica generica formulata in linguaggio comune e non formalizzata.
Che cosa misurano i risultati
I due risultati principali riguardano insiemi distinti valutati nello studio:
| Insieme valutato | Dimostrazioni riportate | Elementi valutati | Ambito |
| Problemi di Erdős | 9 | 353 | Problemi formalizzati in Lean |
| Congetture OEIS | 44 | 492 | Congetture aperte selezionate |
I 353 problemi di Erdős erano quelli formalizzati e disponibili per la valutazione nel repository Formal Conjectures al momento dell’esecuzione. Le 492 congetture OEIS erano una selezione di problemi aperti. Due dei nove problemi di Erdős risolti erano rimasti aperti per 56 anni.
Come funziona la ricerca di dimostrazioni
Gli agenti propongono e modificano il codice della dimostrazione; Lean lo compila e restituisce un riscontro che orienta i tentativi successivi. In questo modo, una proposta plausibile del modello deve superare un controllo meccanico prima di essere considerata una prova formale valida.
La configurazione completa aggiunge una ricerca evolutiva: mantiene più schemi di dimostrazione, li valuta e seleziona quelli da sviluppare. Può inoltre chiamare AlphaProof, un sistema specializzato, per affrontare sottoproblemi. La configurazione di base, invece, ripete modifiche agli schemi usando il riscontro di Lean.
Che cosa mostrano i risultati
Lean verifica che la dimostrazione segua dall’enunciato formalizzato. Non stabilisce da solo se quell’enunciato rappresenti fedelmente la domanda matematica informale da cui deriva: sono due controlli diversi. Per i problemi di Erdős dello studio, i ricercatori riferiscono una revisione esperta delle formalizzazioni.
La maggior parte dei problemi di Erdős valutati è rimasta irrisolta. I successi riportati si concentrano in aree come combinatoria, ottimizzazione convessa e teoria dei numeri, dove le librerie matematiche di Lean sono più mature e i compiti si prestano a essere suddivisi in sottoproblemi.
