Un ricercatore di Microsoft e un collaboratore dimostrano la congettura KLS, formulata 31 anni fa

Microsoft Research ha annunciato il 21 ottobre 2026 che Xinzhi Zhang, ricercatore senior nel suo gruppo di apprendimento automatico e ottimizzazione, e il collaboratore Zhao Song hanno dimostrato la congettura di Kannan–Lovász–Simonovits, un problema di geometria e probabilità in alta dimensione formulato 31 anni fa, grazie a un processo di ricerca con agenti IA diretto da esseri umani.

La congettura e il nuovo limite

La dimostrazione è presentata nel lavoro di 140 pagine Un limite O(1) per la costante KLS, attribuito a Zhao Song e Xinzhi Zhang, inviato per la prima volta ad arXiv il 1º ottobre 2026 e rivisto il 4 ottobre 2026, con Zhang come autore che lo ha inviato. L’abstract afferma che gli autori dimostrano che la costante KLS ψ_n è limitata superiormente da una costante universale C, risolvendo così la congettura, e che dimostrano anche l’esistenza di un limite universale per la costante di Poincaré di ogni misura di probabilità isotropa log-concava.

In termini formali, la congettura, proposta nel 1995, chiede se ogni misura di probabilità isotropa log-concava in uno spazio n-dimensionale abbia una costante di Cheeger limitata inferiormente da una costante positiva universale. In termini più semplici, come spiega il post di Microsoft Research, chiede se, per un’ampia classe di distribuzioni di probabilità in alta dimensione, il miglior taglio piano, o mediante un iperpiano, sia sempre quasi efficace quanto il miglior taglio di qualsiasi forma, con una differenza non superiore a una costante universale, a prescindere dal numero di dimensioni. Poiché la geometria di questi tagli determina la rapidità con cui le passeggiate aleatorie possono esplorare una distribuzione, la congettura svolge un ruolo centrale nella teoria del campionamento in alta dimensione.

Prima di questo lavoro, il miglior risultato noto era l’articolo di 21 pagine La costante KLS è O(log^{1/4} n) di Brayden Letwin, inviato il 27 luglio 2026. Dimostrava che ψ_n è al più pari a una costante moltiplicata per log^{1/4} n, un limite che, come osserva il post di Microsoft Research, continuava a crescere lentamente all’aumentare del numero di dimensioni. Il nuovo risultato vale con un limite fisso, che non varia al variare della dimensione.

L’importanza della congettura era stata riconosciuta ben prima della sua risoluzione. Il post ricorda che la relazione annuale 2017–18 del Mathematical Sciences Research Institute definiva KLS un problema aperto centrale nella geometria convessa in alta dimensione, che il Simons Institute la descriveva come uno dei problemi aperti più importanti della geometria convessa e che Ronen Eldan ne aveva sottolineato le ampie implicazioni negli atti del Congresso internazionale dei matematici del 2022.

Un processo di ricerca con agenti diretto da esseri umani

Secondo il post, gli autori hanno iniziato cercando di migliorare il risultato del luglio 2026. Attraverso un processo strutturato e diretto da esseri umani, con agenti IA, hanno esplorato oltre 100 approcci candidati, molti dei quali richiedevano calcoli complessi con tensori di ordine superiore, e hanno formulato un nuovo criterio matematico che è diventato il fondamento della dimostrazione finale.

Gli autori hanno poi scoperto che il criterio poteva essere applicato ricorsivamente, reinserendo ogni limite migliorato nello stesso argomento per ottenerne uno ancora più stretto. Nella versione del lavoro del 1º ottobre 2026, questo approccio aveva ridotto la dipendenza dalla dimensione al logaritmo iterato, che cresce molto lentamente ma continua comunque a crescere con la dimensione e, pertanto, non risolveva ancora la congettura. Il passaggio finale è consistito nel ripetere l’intero processo di raffinamento ricorsivo, anziché applicarlo una sola volta: un’idea che, secondo il post, è stata ispirata dal precedente lavoro degli autori su algoritmi veloci per la programmazione lineare. Gli autori hanno dimostrato che i piccoli errori introdotti a ogni passaggio si riducono abbastanza rapidamente da mantenere la loro somma entro una costante universale indipendente dalla dimensione, completando la dimostrazione nella versione del 4 ottobre 2026.

Il post afferma che il metodo ricorsivo, la sua applicazione ripetuta e l’argomento basato sul controllo degli errori sono contributi originali dei ricercatori. Gli strumenti di IA hanno contribuito a esplorare approcci candidati, svolgere derivazioni dettagliate, preparare il manoscritto ed eseguire controlli interni della dimostrazione; i ricercatori, invece, hanno determinato la direzione matematica, selezionato le idee promettenti, assemblato gli elementi nell’argomento finale e verificato la dimostrazione. Il post descrive il metodo come una ricerca agentica con selezione iterativa assistita da esseri umani: mentre più agenti esploravano in parallelo varianti di un’idea, il ricercatore esaminava i risultati intermedi, scartava le direzioni poco promettenti e passava il risultato più promettente al ciclo successivo. Prima che emergesse la svolta decisiva, sono stati esplorati circa cento percorsi di ricerca.

In un filone separato del progetto, gli autori hanno tentato più volte, senza indicazioni, di risolvere lo stesso problema con diversi modelli di IA all’avanguardia, utilizzando un budget totale di token all’incirca uguale a quello del processo principale; il post riferisce che questi tentativi non hanno raggiunto l’obiettivo. Secondo il post, il successo finale è dipeso sia dalle capacità dei sistemi di IA sia dal giudizio matematico dei ricercatori. Il post ringrazia Song per il suo contributo al lavoro e Victor Reis e Ishai Menache per le discussioni durante il progetto.

Dimostrazioni indipendenti e verifica automatizzata

Il 4 ottobre 2026, lo stesso giorno in cui è stata pubblicata la dimostrazione completa, Pierre Bizeul, Boaz Klartag e Joseph Lehec hanno pubblicato una dimostrazione di 32 pagine, sviluppata in parallelo, intitolata Presentazione di una dimostrazione della congettura di Kannan-Lovász-Simonovits. L’abstract dell’articolo afferma che «il passaggio cruciale della dimostrazione è il recentissimo criterio di Song e Zhang, che coinvolge derivate di ordine elevato delle medie inclinate», e nei commenti su arXiv si segnala che l’articolo contiene un paragrafo che descrive l’uso dell’IA. L’abstract annovera la KLS, insieme al problema delle sezioni di Bourgain e alla congettura della varianza, tra i motori degli sviluppi matematici nella geometria in alta dimensione degli ultimi decenni.

Krishnakumar Balasubramanian e Shiva Kasiviswanathan hanno pubblicato una dimostrazione distinta, Un limite indipendente dalla dimensione per la costante di Poincaré delle misure isotrope log-concave, presentata per la prima volta il 6 ottobre 2026 e rivista l’8 ottobre 2026. L’abstract descrive una dimostrazione variazionale deterministica con un limite esplicito pari a 25 per la costante di Poincaré di qualsiasi misura di probabilità isotropa e log-concava.

È seguita una formalizzazione in Lean 4 denominata KLS500, che formalizza una costante di Poincaré indipendente dalla dimensione e non superiore a 500 per ogni legge di probabilità isotropa e log-concava. Secondo il repository, lo sviluppo si basa principalmente sull’approccio dei cumulanti e della sospensione di Bizeul, Klartag e Lehec, integrando il criterio tilt-spettrale di Song e Zhang; la sua verifica ha ricostruito 1.710 moduli matematici al livello zero di fiducia del kernel. È stata superata anche la verifica in Lean dell’enunciato esatto della congettura KLS definito da OpenAI, utilizzando la costante di Poincaré universale 500. Il progetto è distribuito con licenza Apache 2.0.

Il post di Microsoft Research descrive le dimostrazioni indipendenti come una delle forme di convalida più solide in matematica, perché dimostrano che un risultato non si basa su un’unica catena di ragionamento. Risolta la congettura, afferma il post, i risultati che in precedenza la assumevano come ipotesi possono ora essere enunciati senza condizioni. Gli autori hanno abbreviato la dimostrazione e verificato in Lean l’argomentazione semplificata; il post riferisce che intendono pubblicare entrambe dopo la revisione finale.