Il paper su Science, pubblicato l’8 ottobre 2026, riporta che AlphaProof Nexus, il sistema di Google DeepMind, ha risolto 9 dei 353 problemi aperti di Erdős valutati. Nello stesso lavoro, il sistema ha dimostrato 44 delle 492 congetture aperte considerate nell’Online Encyclopedia of Integer Sequences (OEIS).
I risultati riportati su Science
I due conteggi riguardano raccolte matematiche distinte: 9 soluzioni su 353 problemi aperti di Erdős e 44 dimostrazioni su 492 congetture dell’OEIS. Due dei problemi di Erdős risolti erano rimasti aperti da 56 anni.
Come si combinano generazione delle prove e Lean
AlphaProof Nexus alterna la generazione di prove basata su un modello linguistico di grandi dimensioni (LLM) alla verifica formale con Lean, un assistente di dimostrazione che controlla i passaggi formali. Il paper riferisce inoltre che un agente di base, alternando generazione e verifica, ha riprodotto i nove risultati sui problemi di Erdős.
Che cosa misurano questi numeri
I risultati descrivono due valutazioni separate: una su 353 problemi aperti di Erdős e l’altra su 492 congetture aperte dell’OEIS. I rispettivi conteggi sono 9 e 44.
