Dalla ricerca di dimostrazioni guidata da esperti alla risoluzione automatizzata di problemi aperti

Abstract degli autori

I modelli linguistici di grandi dimensioni contribuiscono sempre più alla ricerca matematica, in cui i progressi dipendono spesso dall’efficienza nella ricerca di dimostrazioni, da miglioramenti incrementali e da verifiche accurate. Descriviamo Bolzano, un sistema open source multiagente che impiega in parallelo agenti incaricati di trovare dimostrazioni, affiancati da un agente verificatore, e mantiene uno stato della ricerca leggibile dalle persone. Un primo utilizzo manuale su problemi selezionati da esperti ha prodotto 8 risultati, le cui dimostrazioni sono state verificate da esperti del settore. Sulla scorta di questi casi di studio, abbiamo eseguito Bolzano senza indicazioni umane specifiche per i problemi su circa 3.800 problemi aperti estratti da quattro raccolte di articoli, risolvendone circa 200. Un esperimento ha utilizzato articoli accettati a STOC 2026, una delle principali conferenze di informatica teorica. In quell’esperimento abbiamo risposto a quattro domande sollevate negli articoli, come confermato dai loro autori.