Un gruppo di fisici e matematici incaricato di esaminare una dimostrazione prodotta da modelli di intelligenza artificiale di OpenAI ha confermato la validità formale di un risultato riguardante l’esistenza della teoria quantistica pura di Yang–Mills in quattro dimensioni. La verifica costituisce un passaggio significativo per uno dei problemi matematici collegati ai fondamenti del Modello Standard della fisica delle particelle, poiché riguarda la possibilità di costruire rigorosamente una teoria quantistica dei campi a partire da una formulazione reticolare. Il gruppo di valutazione è presieduto dal premio Nobel per la fisica David Gross e comprende Michael Douglas, Arthur Jaffe, Igor Klebanov e Nikita Nekrasov. Il lavoro sottoposto alla valutazione è stato formalizzato mediante Lean, un assistente alla dimostrazione che permette di rappresentare affermazioni matematiche e verificarne i passaggi logici attraverso un sistema di controllo automatico.
La teoria di Yang–Mills descrive una classe di campi di gauge non abeliani fondamentali per la comprensione delle interazioni tra particelle elementari. La sua formulazione quantistica costituisce la base matematica della cromodinamica quantistica, la teoria che descrive l’interazione forte, responsabile del legame tra quark e gluoni. Sebbene le teorie di gauge siano utilizzate con successo nella fisica delle particelle, la costruzione matematica rigorosa della teoria quantistica in quattro dimensioni presenta difficoltà che non possono essere risolte semplicemente attraverso l’efficacia delle previsioni sperimentali. La dimostrazione elaborata dai modelli OpenAI affronta il problema costruendo una teoria quantistica relativistica dei campi che soddisfa gli assiomi di Wightman e deriva come limite di scala della teoria di gauge reticolare di Wilson, per gruppi di gauge compatti, semplici e appropriati alla formulazione esaminata.
OpenAI ha indicato il 9 settembre 2026 come data di produzione di una dimostrazione in linguaggio naturale relativa all’esistenza della teoria di Yang–Mills e il 18 settembre come data di un successivo risultato riguardante la cromodinamica quantistica. La formalizzazione in Lean della dimostrazione di esistenza è stata completata il 16 ottobre e una versione del lavoro è stata consegnata al gruppo di valutazione il 28 ottobre. Nella documentazione resa pubblica il 10 novembre, gli esperti hanno descritto le procedure utilizzate per esaminare il codice, tra cui la ricostruzione dell’ambiente di verifica, il controllo degli assiomi e il confronto tra le formulazioni matematiche indipendenti e quelle implementate nella dimostrazione. L’esito positivo di questi controlli riguarda la coerenza formale della costruzione sottoposta alla verifica, mentre l’interpretazione matematica e fisica completa di un lavoro di tale complessità resta oggetto di ulteriore esame. Gli stessi valutatori hanno chiarito che la verifica informatica non implica una comprensione esaustiva di ogni aspetto della dimostrazione da parte dei revisori.
Il risultato non costituisce ancora la soluzione completa del problema di Yang–Mills e del divario di massa, incluso tra i Millennium Prize Problems del Clay Mathematics Institute. La dimostrazione esaminata non stabilisce infatti l’unicità del limite a volume infinito e non dimostra l’esistenza di un mass gap positivo, ossia di una separazione energetica strettamente maggiore di zero tra lo stato fondamentale e i primi stati eccitati della teoria. Queste condizioni rimangono essenziali per la soluzione completa del problema. Il contributo verificato riguarda dunque una parte specifica e sostanziale della costruzione matematica della teoria quantistica, mostrando al tempo stesso come modelli di intelligenza artificiale, linguaggi di formalizzazione e gruppi scientifici specializzati possano collaborare nella produzione e nella valutazione di dimostrazioni estremamente complesse.
Questo articolo è stato redatto con il supporto di strumenti di intelligenza artificiale (AI)