L’AI Risolve i Problemi di Erdős. Cosa Succede Dopo?

Solo pochi mesi fa, la domanda sembrava prevalentemente filosofica: se l’intelligenza artificiale può aiutare a risolvere problemi matematici aperti, cosa succede all’idea di genio umano?

Quella domanda non è più teorica. Due sviluppi recenti che coinvolgono OpenAI e Google DeepMind suggeriscono che l’AI sta passando da assistente matematico a partecipante matematico. Non nel senso di sostituire i matematici in toto, ma nel senso più preciso e importante di generare, cercare, verificare e a volte scoprire argomenti che possono superare l’esame degli esperti.

Il primo sviluppo è arrivato da OpenAI, che ha annunciato che un modello di ragionamento generale interno aveva fatto una svolta nel problema della distanza unitaria piana, una famosa questione posta da Paul Erdős nel 1946. Il problema chiede quanti paia di punti in un piano possono essere esattamente a una unità di distanza. Per decenni, la credenza prevalente era che le costruzioni a griglia quadrata fossero essenzialmente ottimali. Il modello di OpenAI ha trovato una nuova famiglia di costruzioni che ha smentito quella credenza.

Il secondo è arrivato da ricercatori di Google DeepMind, che hanno pubblicato un articolo intitolato Advancing Mathematics Research with AI-Driven Formal Proof Search. Il loro sistema, AlphaProof Nexus, ha valutato la generazione di prove guidata da AI su problemi di ricerca di livello aperto e ha riferito che il suo agente più forte ha risolto autonomamente 9 dei 353 problemi di Erdős aperti. Ha anche dimostrato 44 delle 492 congetture aperte dall’Enciclopedia online delle sequenze di interi.

Insieme, questi risultati segnano un cambiamento. La storia importante non è che l’AI abbia improvvisamente risolto la matematica. Non l’ha fatto. La storia importante è che i sistemi AI stanno iniziando a operare all’interno del ciclo di ricerca stesso.

Perché i Problemi di Erdős Sono una Seria Prova per l’AI

Paul Erdős è stato uno dei matematici più prolifici della storia, e i problemi associati al suo lavoro occupano un posto speciale nella matematica. Molti sono facili da esprimere, difficili da risolvere e collegati a aree profonde come la combinatoria, la teoria dei numeri, la teoria dei grafi e la geometria discreta.

Questo li rende particolarmente utili come benchmark per il ragionamento AI. Non sono esercizi scolastici. Non sono sempre grandi congetture che scuotono la teoria come l’ipotesi di Riemann. Invece, molti problemi di Erdős si trovano a metà strada dove il progresso dipende dal trovare la giusta connessione, la giusta costruzione o la giusta lemma trascurata.

Questo è esattamente dove l’AI potrebbe essere più utile all’inizio. I sistemi di ragionamento moderni non sono solo calcolatori. Possono esplorare molti percorsi di prova possibili, confrontare strategie parziali, recuperare idee lontane da campi adiacenti e testare se un argomento può essere reso rigoroso.

Il risultato di OpenAI è sorprendente perché il modello non ha semplicemente lucidato una rotta nota. Ha trovato un ponte inaspettato tra geometria discreta e teoria algebrica dei numeri. Questo è il tipo di salto concettuale che i matematici di solito associano a una vera creatività.

OpenAI e la Svolta della Distanza Unitaria

Il problema della distanza unitaria piana è semplice da descrivere. Metti n punti nel piano. Conta quanti paia di punti sono esattamente a una unità di distanza. L’obiettivo è capire quanto grande può essere quel conteggio mentre n cresce.

Per quasi 80 anni, i matematici sospettavano che le migliori costruzioni non avrebbero superato drasticamente gli schemi a griglia quadrata. Il modello di OpenAI ha sfidato quell’assunzione producendo una famiglia infinita di esempi che batte il limite atteso con un miglioramento polinomiale.

Questo conta per due ragioni. In primo luogo, cambia l’immagine matematica. Suggerisce che le costruzioni teoriche dei numeri possono avere più da contribuire alla geometria discreta di quanto molti ricercatori abbiano assunto. In secondo luogo, cambia l’immagine dell’AI. Il modello coinvolto è stato descritto come un modello di ragionamento generale, non come un sistema costruito solo per questo problema specifico.

In altre parole, il sistema sembra aver trasferito il potere di ragionamento in un ambiente di ricerca non familiare. Non ha semplicemente memorizzato una prova nota. Ha generato un risultato che i matematici esterni hanno trattato come un contributo importante.

Google DeepMind e la Ricerca di Prova Formale

L’articolo di Google DeepMind affronta una domanda diversa ma altrettanto importante: come può essere resa affidabile la matematica generata dall’AI?

I modelli linguistici possono produrre argomenti che sembrano eleganti e contengono errori sottili. Nella prosa normale, quegli errori possono essere difficili da rilevare. In matematica, un passo sbagliato può invalidare l’intera prova. È per questo che sistemi di prova formali come Lean sono importanti. Lean non si cura se un argomento suona persuasivo. Ogni passo logico deve essere verificato.

AlphaProof Nexus utilizza quella costrizione come parte del flusso di lavoro. Gli agenti AI generano tentativi di prova in Lean, ricevono feedback dal compilatore, revisionano il loro approccio e continuano la ricerca. La versione più forte coordina sottogenti e utilizza strumenti di prova più avanzati per focalizzare la ricerca.

Il risultato di DeepMind è particolarmente importante perché collega il ragionamento AI alla verifica. Il sistema non deve essere affidato allo stesso modo in cui un chatbot di linguaggio naturale deve essere affidato. La sua prova o compila o non compila.

Cosa Significa Ciò per la Ricerca Matematica

La lezione attuale non è che i matematici sono obsoleti. È che il collo di bottiglia nella matematica potrebbe stare cambiando.

Storicamente, un ricercatore doveva fare quasi tutto: formulare il problema, esaminare la letteratura, testare idee, costruire la prova, verificare ogni passo e comunicare il risultato. L’AI ora minaccia di ridistribuire quel lavoro. Alcune parti del flusso di lavoro potrebbero diventare più veloci, più economiche e più automatizzate.

• L’AI può esplorare molte rotte di prova prima che un umano si impegni in una.
• I sistemi formali possono verificare passaggi che altrimenti richiederebbero una lenta verifica degli esperti.
• I ricercatori possono utilizzare l’AI per cercare attraverso sottocampi matematici lontani.

Ciò potrebbe produrre uno stile di ricerca nuovo. Invece di chiedere all’AI una risposta, i matematici potrebbero sempre più supervisionare flotte di agenti di prova. Il ruolo umano diventa meno come un calcolatore e più come un direttore di ricerca: scegliere i problemi giusti, interpretare i risultati, rilevare la significatività concettuale e decidere quali percorsi meritano un’attenzione più profonda.

I Limiti Sono Ancora Reali

È importante non esagerare il momento. Il sistema di Google DeepMind ha risolto 9 dei 353 problemi di Erdős tentati. È impressionante, ma significa anche che la maggior parte è rimasta irrisolta. Il risultato della distanza unitaria di OpenAI è un punto di riferimento, ma non implica che ogni famosa congettura sia ora a portata di mano.

I sistemi AI ancora lottano quando un problema richiede un nuovo quadro concettuale, quando la matematica pertinente è scarsamente formalizzata o quando una prova dipende da lunghe catene di intuizione che non possono essere facilmente decomposte in passaggi di ricerca. Le librerie di prove formali sono anche disomogenee. Le aree con una copertura Lean matura sono più accessibili agli agenti AI rispetto alle aree in cui il materiale fondamentale deve ancora essere codificato.

• I sistemi rimangono dipendenti dalla selezione e interpretazione dei problemi umani.
• La formalizzazione può essere difficile quando le definizioni sono ambigue o in fase di sviluppo.
• I tentativi di prova generati dall’AI possono ancora nascondere lavoro difficile all’interno di affermazioni di aiuto non dimostrate.

Questi limiti non sono fallimenti. Chiariscono dove devono avvenire i prossimi progressi. Agenti di teoremi migliori, librerie formali più ricche, flussi di lavoro di verifica più forti e interfacce uomo-macchina più efficaci saranno tutti importanti.

Cosa Succede Dopo che l’AI Risolve i Problemi di Erdős?

Il futuro più probabile a breve termine non è un momento drammatico in cui l’AI risolve tutta la matematica. È un’espansione costante della ricerca assistita dall’AI in domini con enunciati di problema puliti, librerie formali solide e grandi quantità di lavoro precedente frammentato.

La combinatoria, la teoria dei grafi, la teoria dei numeri, l’ottimizzazione e la geometria discreta sono obiettivi naturali precoci. Questi campi spesso contengono problemi in cui la domanda è concisa, ma la soluzione dipende dal cucire insieme idee da posti lontani. L’AI è ben adattata a quel tipo di ricerca.

Nel tempo, lo stesso modello potrebbe estendersi oltre la matematica. Se un modello può tenere insieme un argomento difficile, testare affermazioni intermedie e collegare idee attraverso campi, quelle capacità contano nella fisica, nella biologia, nella scienza dei materiali, nella crittografia e nella ricerca sull’AI stessa.

La conseguenza più profonda è culturale. La matematica ha sempre valorizzato la prova, ma ha anche valorizzato il gusto: la capacità di sapere quale domanda è importante, quale astrazione vale la pena inventare e quale risultato cambia la forma di un campo. Mentre la ricerca di prove diventa più automatizzata, il gusto potrebbe diventare più importante, non meno.

Conclusione: Il Genio Si Sposta Verso l’Alto

La risposta alla domanda successiva è ora più chiara. Se l’AI può risolvere problemi matematici aperti, il genio umano non scompare. Si sposta verso l’alto.

La competenza rara non sarà la capacità di macinare attraverso ogni passo tecnico da solo. Sarà la capacità di fare le domande giuste, inquadrare le astrazioni giuste, giudicare il significato dei risultati scoperti dalle macchine e guidare i sistemi AI verso problemi che contano.

La svolta della distanza unitaria di OpenAI e i risultati della ricerca di prova formale di Google DeepMind non chiudono il libro sulla creatività matematica umana. Aprono un nuovo capitolo in cui i matematici possono lavorare con sistemi che possono esplorare il territorio più velocemente di qualsiasi mente individuale.

Il futuro della matematica potrebbe non appartenere agli esseri umani o alle macchine da soli. Potrebbe appartenere ai ricercatori che imparano a farli pensare insieme.