Una voce su un risultato inedito di OpenAI ha cambiato il calendario di tre ricercatori MIT prima che la prova IA fosse esaminabile. Dor Minzer e i dottorandi Yumou Fei e Shuo Wang seppero l'11 settembre di un risultato imminente su Unique Games. Il 14 pubblicarono 95 pagine ancora grezze su un teorema collegato ma diverso. OpenAI annunciò la raccolta il 6 ottobre, rivendicando la dimostrazione della congettura.
La svolta umana risaliva ad aprile e il gruppo stava preparando la spiegazione. La prevista uscita aziendale rese urgente la priorità, a scapito dell'esposizione. I teoremi non si annullano e nessun preprint sostituisce la revisione indipendente.
Due risultati distinti
Subhash Khot introdusse Unique Games nel 2002. Vertici collegati da archi ricevono etichette; ogni arco impone una permutazione. Sapere l'etichetta di un estremo determina esattamente quella ammessa all'altro. Questa corrispondenza uno a uno spiega il nome.
La congettura riguarda la difficoltà dell'approssimazione. Informalmente è difficile distinguere istanze quasi interamente soddisfacibili da quelle con solo una piccola frazione soddisfacibile. Non significa assenza di soluzioni, ma limiti degli algoritmi generali efficienti su famiglie precise.
Nell'ottimizzazione si accetta un'approssimazione quando l'ottimo esatto costa troppo. Unique Games collega molte garanzie a barriere intrinseche. Il quadro di Raghavendra del 2008 dimostra condizionalmente l'ottimalità della programmazione semidefinita per ampie classi: risolvere un rilassamento geometrico e arrotondare a scelte discrete.
Il teorema MIT riguarda completezza perfetta, tutte le condizioni iniziali soddisfacibili. In un gioco 2-a-1, un'etichetta permette due scelte compatibili dall'altro lato; nel 4-a-1 quattro. È più debole dell'originale 2-a-1, ma raggiunge un caso esatto non direttamente coperto da Unique Games ordinario.
Tutte non significa quasi tutte
Minzer e collaboratori avevano raggiunto completezza quasi perfetta nel 2018. Un piccolo divario può impedire riduzioni che richiedono un punto iniziale interamente soddisfacibile. L'estremo esatto non è cosmetico.
Fei e Wang iniziarono nel 2025. Un nuovo codice correttore offriva un ingrediente promettente, ma integrarlo nella riduzione falliva. La svolta di aprile combinò equazioni quadratiche, livello intermedio di verifica e verificatore interno con codifica di tipo Grassmann.
Sono tecniche di prove probabilisticamente verificabili, che controllano poche posizioni casuali di una prova lunga. La riduzione deve preservare il divario tra casi accettati e respinti. Conta l'interazione dei livelli, non solo il codice.
Una conseguenza riguarda la colorazione. Anche promettendo che il grafo ammetta tre colori, trovare una colorazione valida con qualsiasi numero fisso di colori resta NP-difficile. Aggiungerne non garantisce un metodo generale efficiente. Il teorema riguarda anche insiemi indipendenti in alcuni ipergrafi, con archi che connettono più di due vertici.
È un contributo distinto dalla congettura usuale rivendicata da OpenAI. Gli autori difendevano una via indipendente, non un duplicato.
Il costo di pubblicare in tre giorni
Il gruppo disse che la matematica era completa ma non la presentazione desiderata. Il preprint ECCC del 14 settembre aveva 95 pagine. Minzer descrisse le sezioni dopo la sesta come quasi prive di raccordi: definizioni e prove restavano, con poca guida.
L'esposizione è infrastruttura scientifica. Motivazioni, transizioni, confronti e spiegazioni permettono verifica e riuso. Ottenere una data rapida lasciava questo debito.
Il gruppo non conosceva argomento, modello, pretesa esatta o calendario aziendale. Non era una gara ordinaria con tempi umani comparabili. La produzione attesa della macchina dirottava già il lavoro.
La quantità aggiunge un problema di revisione
OpenAI dichiara circa 4.000 problemi tentati e 722 manoscritti su 377 domande. Una raccolta contiene 40 prove di informatica teorica. Tentativi, manoscritti, domande e prove sono unità diverse, non conteggi intercambiabili di problemi risolti.
Il calcolo medio equivaleva a circa tre ore di ragionamento ChatGPT Pro per risultato. Non è costo esatto di Unique Games né budget uniforme. Circa metà era formalmente verificata all'annuncio secondo l'azienda; completare il resto era una previsione.
Il manoscritto rivendica una riduzione esplicita deterministica polinomiale da 3SAT a istanze non pesate, con artefatti Lean. Le conseguenze su tagli, coperture, ordinamento, eliminazione, clustering e vincoli dipendono dal teorema e da riduzioni precedenti.
OpenAI non lo presentava come revisione tradizionale. Riconosceva riferimenti ed esposizione da migliorare e prometteva aiuto alla comprensione. Output pubblici possono essere prove importanti senza valutazione comunitaria conclusa.
Lean controlla una proposizione formale
Lean verifica passi codificati da ipotesi e regole codificate. È più forte dell'autodichiarazione del modello, ma gli esperti devono confrontare enunciato e congettura, ipotesi importate e collegamenti tra codice e testo.
Ordine dei quantificatori e dipendenza dell'alfabeto dagli errori sono sensibili. Cambiarli può indebolire una proposizione simile. Completezza, solidità, esplicitezza e tempo polinomiale devono corrispondere alla pretesa standard.
Una derivazione controllata non spiega automaticamente idea decisiva, novità, credito o consenso. Verifica e comprensione sono fasi diverse. Anche il testo umano frettoloso richiede lettura esperta e revisione.
La riproducibilità è stratificata. Lean e dipendenze possono consentire di ripetere il controllo. Il modello interno senza nome non è pubblico; sintesi e statistiche non forniscono tutti i prompt, campionamenti e interventi. Riprodurre la scoperta è altro.
Ora servono controlli indipendenti dell'allineamento OpenAI, un manoscritto MIT chiaro e uscite a scala macchina esaminabili. L'evento ha già cambiato tempi e priorità. Il progresso duraturo dipende dal trasformare output verificati in spiegazioni che altri possano esaminare, adattare e capire.