DeepMind: nove prove, novità da verificare

Una dimostrazione matematica può essere elegante e nascondere comunque un passaggio mancante, che nessuno individua per anni. L’agente di Google DeepMind AlphaProof Nexus ha prodotto dimostrazioni per nove problemi posti da Paul Erdős, verificando ogni passaggio con un software. Il lavoro è apparso per la prima volta in un preprint di maggio (arXiv ) e, dopo la revisione tra pari, è stato pubblicato su Science l’8 ottobre (Science). Il software poteva confermare la correttezza logica, ma stabilire se quelle dimostrazioni contenessero qualcosa di nuovo spettava ai matematici.

Un arbitro che non si lascia incantare

I chatbot sanno scrivere testi matematici convincenti: un paragrafo sicuro di sé può coprire un passaggio mancante, che solo un lettore attento riesce a individuare. AlphaProof Nexus aggira il problema lavorando in Lean, un linguaggio di programmazione che permette di formulare definizioni, enunciati e dimostrazioni con una precisione tale da renderli verificabili da un computer.

Lean funziona come un arbitro che legge ogni riga di una dimostrazione completa applicando regole fisse: lo stile non conta e basta che un passaggio non discenda da quelli precedenti perché la prova fallisca, per quanto elegante sia il resto.

Il gruppo descrive l’agente come un sistema che cerca dimostrazioni formalizzate in Lean; i ricercatori gli hanno anche dato accesso ad AlphaProof, un precedente sistema di DeepMind progettato appositamente per le dimostrazioni. Nei test, però, una configurazione più semplice ha ottenuto gli stessi risultati: un modello linguistico abbinato a Lean, senza AlphaProof, ha comunque trovato tutte e nove le dimostrazioni dei problemi di Erdős (The Decoder). Per quei problemi, la componente specialistica si è rivelata superflua.

L’articolo presenta dimostrazioni accettate per i nove enunciati di Erdős e per 44 congetture (affermazioni ritenute vere ma mai dimostrate) dell’Online Encyclopedia of Integer Sequences, un vasto catalogo di sequenze numeriche (Science). Tra i risultati di Erdős c’è una domanda in due parti sui numeri interi, posta da Erdős e András Sárközy nel 1970 e rimasta aperta per oltre mezzo secolo (ABC).

Ciò che l’arbitro non può vedere

La garanzia di Lean ha confini precisi: conferma che una dimostrazione prova l’enunciato esattamente nella forma in cui è scritto nel codice. Restano fuori tre questioni: se il codice rispecchi ciò che Erdős intendeva, se qualcuno avesse già risposto alla domanda molto tempo fa e se la risposta insegni qualcosa.

Il problema del 1970 mostra perché le ultime due questioni contino: la seconda parte implica la prima, perciò basta una dimostrazione per risolverle entrambe. Dopo la diffusione delle prove dell’agente, è emerso che una modifica modesta a una costruzione contenuta nell’articolo originale del 1970 rispondeva già a entrambe le parti (arXiv). Le dimostrazioni dell’agente erano corrette; semplicemente, il problema era più vicino alla soluzione di quanto lasciasse intendere la sua etichetta di «aperto».

Per cogliere queste sfumature servono esperti del settore: Gergely Bérczi, matematico dell’Aarhus University in Danimarca e coautore dello studio, ha contribuito a scegliere i problemi adatti, a convalidare le soluzioni (Aarhus University) e a redigere versioni delle dimostrazioni comprensibili ai lettori. Lean ha verificato ogni passaggio; Bérczi e i colleghi hanno valutato che cosa significasse l’insieme.

Questa divisione del lavoro distingue lo studio da un risultato raggiunto il mese scorso: allora Claude, il sistema di Anthropic, ha tradotto in Lean la dimostrazione già nota dell’ultimo teorema di Fermat (To Brief). Una traduzione di una dimostrazione famosa non solleva dubbi sulla novità. Una ricerca tra enunciati considerati aperti sì, e in quel caso verificare la novità diventa il passaggio decisivo.

Il gruppo ha pubblicato i file delle dimostrazioni, così che altri possano sottoporli allo stesso verificatore (GitHub). Il risultato dello studio è circoscritto: un agente di IA ha prodotto dimostrazioni verificabili da una macchina per alcuni enunciati che i matematici consideravano ancora aperti, con una garanzia valida per quegli enunciati così come sono formulati in Lean. Spettava comunque ai matematici che le hanno lette stabilire che cosa ciascuna dimostrazione aggiungesse alla disciplina.