OpenAI afferma che i suoi modelli hanno confutato l'ipotesi del tempo esponenziale e dimostrato la congettura di Kakeya

OpenAI ha annunciato il 26 ottobre tre risultati scientifici prodotti dai suoi modelli interni: una confutazione dell’ipotesi del tempo esponenziale (ETH), un pilastro dell’informatica teorica, una dimostrazione in ogni dimensione della congettura di lisciamento locale, che comporta quella di Kakeya, e una dimostrazione dell’esistenza di teorie quantistiche dei campi, inclusa la cromodinamica quantistica. Sono affermazioni, non ancora acquisizioni: la comunità scientifica sta appena iniziando a esaminarle.

Tre risultati, tre ambiti

In informatica teorica. L’ETH postula, per dirla in breve, che il problema 3-SAT (decidere se una formula logica può essere soddisfatta) non possa essere risolto in tempo sotto-esponenziale. È largamente ammessa e serve da ipotesi di partenza a centinaia di articoli, che ne deducono che un problema è difficile. La prepubblicazione di OpenAI, datata 25 ottobre, descrive un algoritmo deterministico che conta esattamente le soluzioni delle formule di larghezza fissa in tempo sotto-esponenziale e in spazio polinomiale; il caso di 3-SAT confuterebbe l’ETH. Secondo OpenAI, il modello ha trovato questa dimostrazione il 16 ottobre e essa è stata formalizzata in Lean, un assistente di dimostrazione che verifica meccanicamente ogni passaggio, il 17 ottobre.

In matematica. La congettura di lisciamento locale, proposta da Sogge nel 1991, riguarda la focalizzazione delle onde. Era stata dimostrata in dimensione 2 nel 2019 (Guth, Wang e Zhang), e la congettura di Kakeya in dimensione 3 nel 2025 (Wang e Zahl). I modelli di OpenAI ne propongono una dimostrazione in ogni dimensione, fondata su un’equazione alle derivate parziali ausiliaria. Il registro del repository è un po’ più prudente dell’annuncio su una delle conseguenze: parla delle stime di restrizione di Stein «nell’interno» del dominio congetturato.

In fisica. Il terzo risultato è una dimostrazione matematicamente rigorosa dell’esistenza di certe teorie quantistiche dei campi in quattro dimensioni, inclusa la QCD, che descrive l’interazione forte tra quark e gluoni. Include l’esistenza della teoria di Yang-Mills pura, che fa parte di uno dei problemi del millennio dell’istituto Clay. Né il testo né la formalizzazione sono pubblicati: il gruppo di fisici ha scelto di redigere autonomamente una presentazione.

Un nuovo metodo di pubblicazione

OpenAI presenta questi manoscritti come «dati di ricerca grezzi» e ha chiesto a specialisti di ciascun ambito di organizzare il loro esame. Per l’ETH, il gruppo è guidato da Russell Impagliazzo e Ramamohan Paturi, che hanno formulato l’ipotesi, e da Ryan Williams (MIT). Per la fisica, dal Nobel David Gross, con Michael Douglas, Arthur Jaffe, Igor Klebanov e Nikita Nekrasov. I partecipanti non firmano alcun accordo di riservatezza, non sono retribuiti e parlano a titolo personale. OpenAI dichiara di non rivendicare alcun credito accademico e si è impegnata, su richiesta del gruppo, a finanziare una conferenza sulle conseguenze del risultato.

Ryan Williams ha annunciato l’esame parlando di una confutazione «asserita» dell’ETH, e precisa che il gruppo ha richiesto la pubblicazione di tutti i dati grezzi, PDF e codice Lean compresi.

Perché la prudenza è necessaria

La formalizzazione in Lean è un argomento forte, ma garantisce solo ciò che è stato formalizzato: bisogna ancora verificare che gli enunciati verificati dalla macchina corrispondano agli enunciati che i ricercatori hanno in mente. La cronologia di OpenAI ricorda anche che un errore resta possibile: il 7 ottobre, l’azienda ha ritirato tre manoscritti da una pubblicazione precedente, invalidati da un errore di segno, e ne ha corretti quattordici altri.