Congetture con LLM vs verifica di prove: chi vince

Tra il secondo e il terzo caffè, parecchi teorici della complessità hanno letto di recente una frase che non si aspettavano: un algoritmo deterministico che conta le assegnazioni soddisfacenti di una formula booleana arbitraria in tempo circa 2^(n/√(log n)) — subesponenziale, nel senso tecnico preciso che smentisce la Exponential Time Hypothesis, una delle ipotesi portanti del settore. L'affermazione non è uscita su arXiv da un gruppo universitario. Viene da un laboratorio di IA, con la dimostrazione sviluppata in collaborazione con un large language model. Qualunque cosa si pensi dell'annuncio, segna il momento in cui la generazione di congetture — macchine che propongono nuova matematica invece di limitarsi a valutarla — è uscita dalla fase di demo.

Il laboratorio ha presentato tre risultati: la bomba di complessità descritta sopra, una dimostrazione dichiarata della congettura di Kakeya in tutte le dimensioni e un risultato di fisica descritto come un «completamento unificato del Modello Standard», trattenuto in attesa della verifica formale. La reazione ha seguito uno schema noto: stupore autentico per la sostanza, irritazione altrettanto autentica per il packaging. I critici l'hanno paragonata a un produttore di biciclette che annuncia le proprie vittorie nelle corse ciclistiche. Calzante — eppure la sostanza merita uno sguardo più lento, perché in questo annuncio c'è una lezione concreta sui due modi molto diversi in cui i modelli linguistici toccano oggi la matematica, e su quale dei due dovresti davvero fidarti.

Cosa afferma davvero l'annuncio sulla matematica dell'IA

Partiamo dal risultato di complessità, perché è quello con le poste più chiare. La Exponential Time Hypothesis afferma, grosso modo, che il 3-SAT non può essere risolto in tempo 2^o(n) — nessun algoritmo può essere significativamente subesponenziale nel numero di variabili. Centinaia di articoli in complessità parametrizzata e fine-grained si appoggiano all'ETH per dimostrare limiti inferiori; è il tipo di ipotesi su cui si impila una carriera intera di teoremi del tipo «condizionale all'ETH». Il nuovo preprint descrive un algoritmo di conteggio deterministico per formule k-CNF che usa spazio polinomiale e gira in tempo 2^(n/(log n)^(1/2+o(1))) moltiplicato per un fattore polinomiale. Quell'esponente è o(n), esattamente ciò che l'ETH vieta. L'algoritmo resta spaventosamente lento — nessuno lo eseguirà mai su un'istanza reale — ma asintoticamente è decisivo. Se la dimostrazione regge, un'ipotesi che ha strutturato due decenni di argomenti sui limiti inferiori semplicemente smette di esistere.

La seconda affermazione riguarda la congettura di Kakeya, un problema di teoria geometrica della misura sugli insiemi più piccoli che contengono un segmento unitario orientato in ogni direzione. Il caso tridimensionale è caduto solo nel 2025, con una celebre dimostrazione di Hong Wang e Joshua Zahl che molti hanno considerato il coronamento di una carriera. L'annuncio sostiene una dimostrazione in tutte le dimensioni, che assorbirebbe interamente quel risultato. Il terzo, in teoria quantistica dei campi, è il più vago dei tre: descritto come un «completamento unificato del Modello Standard» ma non ancora rilasciato, in apparenza in attesa di una formalizzazione verificata a macchina. I fisici che hanno letto i teaser sospettano qualcosa della famiglia delle costruzioni in stile grande unificazione piuttosto che una vera teoria del tutto, e la formulazione si è guadagnata qualche giustificato sopracciglio alzato.

Due cose sul rilascio meritano un riconoscimento. Il laboratorio ha coinvolto matematici e fisici al lavoro prima di rendere pubblico l'annuncio — una risposta diretta alle polemiche seguite a un precedente annuncio matematico più maldestro, dopo il quale Terence Tao e altri hanno chiesto pubblicamente proprio questo tipo di coinvolgimento. E il risultato di fisica è stato trattenuto fino al completamento della formalizzazione, che è l'ordine di priorità corretto. Restano però domande senza risposta: nessuno fuori conosce il conto del calcolo, se gli stessi fondi destinati a ricercatori umani avrebbero prodotto gli stessi teoremi, o se un laboratorio a scopo di lucro continuerà a finanziare lavoro guidato dalla curiosità quando gli azionisti avranno voce in capitolo. C'è anche il circolo scomodo che i critici hanno segnalato subito: questi modelli sono addestrati in parte sulle domande, le bozze e i post nei forum della stessa comunità di ricerca che ora è chiamata ad applaudire l'output.

Verifica di prove vs generazione di congetture: due lavori diversi

Tolto l'hype, ogni sistema di IA per la matematica svolge uno di due compiti. Il primo è la verifica di prove: data una dimostrazione candidata, decidere se è valida. Il secondo è la generazione di congetture: dato un ambito di problemi, proporre cosa valga la pena tentare — un lemma, una costruzione, un algoritmo, un controesempio. Sembrano due metà della stessa abilità. Non lo sono. Sono problemi computazionali diversi, con oracoli diversi, modalità di errore diverse e profili di fiducia radicalmente diversi, e confonderli è il modo in cui finisci per sopravvalutare un comunicato stampa o per liquidare progressi reali.

La verifica ha un oracolo. Una dimostrazione scritta in Lean o compila contro il kernel oppure no, e il kernel non si cura di quanto sicuro sembrasse l'autore. La verifica fallisce rumorosamente — un blocco di tattiche rifiutato non ha ambiguità. La generazione non ha oracolo. Una congettura proposta può essere vera, falsa, banalmente vera, o vera ma pubblicata nel 1987 con notazione diversa. La generazione fallisce in silenzio, e le sue modalità di errore sono sociali: sciocchezze dal suono plausibile, oppure risultati genuini travestiti da novità. La qualità qui si misura in importanza e originalità, proprietà definite dal gusto umano e non da un criterio decidibile.

Perché la generazione è diventata improvvisamente abbastanza buona da contare? Perché i modelli di ragionamento moderni sono addestrati su lunghe catene di pensiero, non solo guidati a produrle con il prompt — il reinforcement learning su ricompense verificabili, soprattutto in matematica e codice dove le risposte si possono controllare meccanicamente, ha insegnato a questi sistemi a cercare davvero in uno spazio di passi invece di completare un testo un token alla volta. Ecco l'analogia che terrei a mente: il verificatore di prove è un compilatore, il generatore di congetture è un progettista. Entrambi sono preziosi. Non lasceresti mai, mai, che il progettista certifichi il proprio lavoro.

Una dimostrazione che non sai verificare è un sermone; una congettura che non sai testare è una voce di corridoio.

Dove vince la verifica automatica delle prove

Il verificatore vince ovunque esista una verità di riferimento formale e l'artefatto da esaminare sia troppo lungo o noioso da controllare riga per riga a mano. Lean 4 e la sua libreria della comunità Mathlib sono diventati l'arena di riferimento: scrivi definizioni e dimostrazioni in un linguaggio di programmazione, e un kernel piccolo e verificabile separatamente decide se ogni passo di inferenza è lecito. La base di calcolo fidata è minuscola rispetto alla montagna di matematica costruita sopra, ed è esattamente l'asimmetria che vuoi.

Il ciclo pratico è questo: il modello abbozza passi di prova a livello di tattiche, il kernel accetta o rifiuta ciascuno, e i messaggi di rifiuto tornano come contesto per il tentativo successivo. È il contesto in cui vincolare l'output del modello a una grammatica rigida ripaga subito — campioni solo tattiche sintatticamente valide, quindi intere classi di allucinazioni diventano impossibili per costruzione. Un esempio minimo, del tipo di lemma che oggi un modello sbriga in pochi secondi:

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

Nota cosa mostra l'esempio sulla divisione dei compiti. La mossa creativa è scegliere il testimone k + l; la mossa di verifica è ring che controlla l'algebra. Umani e modelli sono entrambi bravi nella prima. Solo il kernel è affidabile nella seconda, e non si stanca mai, non scorre in fretta e non giudica a sensazione. L'elemento più credibile dell'intero annuncio è proprio questo filtro: l'affermazione che l'articolo di fisica sia stato trattenuto fino al completamento della formalizzazione in Lean. Se il resoconto è accurato, è il flusso di lavoro che funziona come previsto — la macchina propone, la macchina giudica, e il comunicato stampa aspetta il proprio turno.

Dove vince la generazione di congetture

La generazione vince ovunque lo spazio di ricerca sia combinatorio e la valutazione sia economica. FunSearch di DeepMind ha fissato lo schema nel 2023: un modello linguistico propone ipotesi a forma di programma, un valutatore veloce le punteggia, e un ciclo evolutivo tiene le migliori — un impianto che ha prodotto nuove costruzioni per i cap set e euristiche di bin packing migliori di decenni di messa a punto a mano. AlphaEvolve ha spinto l'idea oltre e, tra gli altri risultati, ha tolto una moltiplicazione a un algoritmo di moltiplicazione di matrici 4×4 che resisteva dall'epoca di Strassen. Nessuno sostiene che questi sistemi capiscano la geometria. Non ne hanno bisogno. Devono proporre, e il valutatore deve essere onesto.

L'algoritmo sull'ETH si adatta a questo schema in modo quasi sospetto. Lo spazio delle «idee algoritmiche» è enorme, e i ricercatori umani lo esplorano con forti pregiudizi — che è un modo gentile per dire punti ciechi. Una costruzione che richiede di comporre un particolare trucco di rappresentazione con una specifica struttura di ricorsione può restare inesplorata per trent'anni semplicemente perché il percorso di ricerca di nessuno è mai passato da quelle parti. Una ricerca esaustiva, senza pregiudizi e un po' ottusa è esattamente ciò che portano in tavola le macchine. La stessa logica alimenta i cicli di genera-e-confuta: proponi una congettura, prova subito a demolirla con una ricerca computazionale di controesempi su casi piccoli. La maggior parte delle congetture muore in pochi minuti, ed è un bene — ogni confutazione affina la proposta successiva, e i sopravvissuti sono quelli che meritano il pomeriggio di un essere umano.

C'è anche un'asimmetria psicologica che merita rispetto. La dimostrazione tridimensionale di Kakeya di Wang e Zahl ha richiesto anni di lavoro concentrato al vertice del campo. Se una ricerca assistita da modelli avesse davvero prodotto un argomento valido in tutte le dimensioni, con ogni probabilità avrebbe trovato un percorso diverso attraverso il paesaggio — non necessariamente più profondo, ma diverso. La diversità è esattamente ciò a cui serve la ricerca. Il pericolo non è che le macchine generino congetture; è che qualcuno pubblichi una congettura generata senza gli strumenti per sostenerla. Il che ci porta alla parte della pipeline che devi davvero costruire.

Costruire un ciclo di verifica per le dimostrazioni generate dall'IA

Se vuoi i vantaggi della matematica generata da macchine senza l'imbarazzo, il flusso di lavoro conta più del modello. Ecco la pipeline che eseguirei, in ordine:

1. Genera ampiamente e a basso costo. In questa fase la diversità batte la profondità; vuoi copertura dello spazio delle idee, non un unico tentativo rifinito.
2. Deduplica rispetto alla letteratura. Il recupero su arXiv e MathOverflow intercetta l'errore più comune: una «nuova» congettura che è un risultato noto con una notazione inusuale.
3. Applica filtri empirici economici. Testa numericamente i casi piccoli, cerca controesempi con il calcolo e lascia morire in fretta le affermazioni palesemente false.
4. Formalizza i sopravvissuti. Lean, Isabelle o Rocq — scegli l'assistente di dimostrazione che preferisci, ma sappi che questo è il passo costoso e che una dimostrazione in linguaggio naturale è uno schizzo, non un risultato.
5. Revisione umana per novità e impostazione. Conta davvero? L'enunciato è quello giusto? I modelli ottimizzano ciò che è dimostrabile; gli umani decidono ciò che vale la pena dimostrare.

La collaborazione annunciata ha seguito più o meno questa forma — i ricercatori sono stati coinvolti prima del rilascio, di fatto occupando il passo cinque. È un miglioramento reale rispetto al vecchio approccio «pubblica un preprint e lascia che i social lo arbitrino». Ma nota l'asimmetria della pipeline: i passi da uno a tre sono economici e scalano con il calcolo, il passo quattro è il collo di bottiglia e il passo cinque non scala affatto. Se costruisci strumenti in questo ambito, spendi sul collo di bottiglia — migliore autoformalizzazione, feedback di errore più efficace verso il generatore — non su un generatore più grande e più sicuro di sé.

Perché i matematici umani continuano a custodire la correttezza

Nessun verificatore può dirti che un teorema conta. La scelta dei problemi è gusto, e il gusto è una tecnologia sociale costruita in decenni — seminari, rapporti dei revisori, il lento consenso su quali domande aprono porte e quali sono vicoli ciechi. Lo scetticismo della comunità di ricerca verso gli annunci dei fornitori non è mera difesa corporativa; è un sistema immunitario, e i sistemi immunitari a volte reagiscono in eccesso proprio perché la sottoreazione è fatale.

Poi c'è la provenienza. Questi modelli sono addestrati sulle domande, le bozze e i post nei forum della stessa comunità, il che fa emergere la scomoda possibilità che una «scoperta» celebrata sia una ricombinazione di cose che i suoi futuri revisori hanno scritto. La paura di farsi battere dal proprio strumento non è paranoia — è un problema di tracciabilità dei dati, e finché i laboratori non sapranno dimostrare la provenienza, i revisori umani restano gli unici rilevatori di plagio che funzionano. Aggiungi la politica dei crediti — chi viene invitato a verificare, i nomi che compaiono nell'annuncio, le accuse di favoritismo — e capisci perché il filtro umano non si può eliminare. Scegliere cinque scienziati illustri per benedire un risultato è tanto un atto politico quanto epistemico.

Un'ultima cautela per chi è tentato di leggere le classifiche come misura della capacità di ricerca: le medaglie d'oro nelle competizioni misurano le prestazioni su problemi costruiti per essere risolvibili in ore. La ricerca ha la distribuzione opposta — problemi scelti proprio perché nessuno sa se siano risolvibili. È la stessa ragione per cui i benchmark non colgono gran parte del lavoro reale nell'ingegneria del software: la metrica premia il problema confezionato, non quello disordinato. Un modello che eccelle nei problemi delle olimpiadi ha dimostrato qualcosa di vero. Non ha dimostrato giudizio.

La raccomandazione: fidati del ciclo, non del modello

Ecco la mia posizione, detta chiaramente. La generazione di congetture è reale, utile e migliorerà; la generazione di congetture non verificate non vale nulla, e le dimostrazioni in linguaggio naturale senza un supporto formale vanno trattate come marketing fino a prova contraria. La verifica delle prove vince ogni volta che l'artefatto deve essere creduto. La generazione vince ogni volta che il collo di bottiglia è l'immaginazione e non il rigore. Gli annunci che contano sono quelli in cui le due cose sono state fissate insieme.

Quindi tratta il modello come un collaboratore junior prolifico, con energia infinita e nessun giudizio: tutto ciò che ti consegna passa dall'assistente di dimostrazione prima di entrare nell'articolo, e da un umano con gusto prima di entrare nell'introduzione. Se sei un ricercatore, impara bene un assistente di dimostrazione — la formalizzazione è il collo di bottiglia, e chi sa guidarla sta per avere molto da fare. Se costruisci strumenti, costruisci il ciclo, non la demo. E quando arriverà il prossimo grande annuncio, salta il comunicato stampa, apri il preprint e controlla se esiste il repository Lean. Le affermazioni che sopravvivono sono quelle che arrivano già verificate a macchina.