Fabio Ciotti
In queste settimane alcuni risultati ottenuti in ambito matematico da modelli linguistici top tier con capacità di ragionamento sono stati al centro del dibattito della variegata comunità scientifica che si occupa di LLM, IA e dintorni. Da un lato OpenAI ha annunciato che un proprio modello interno ha confutato una congettura centrale di geometria discreta, ossia la convinzione (radicata da quasi ottant’anni nel problema delle distanze unitarie di Erdős, posto nel 1946) che le configurazioni a griglia quadrata fossero essenzialmente ottimali per massimizzare il numero di coppie di punti a distanza unitaria; il modello ha fornito una famiglia infinita di controesempi che produce un miglioramento polinomiale rispetto al limite inferiore originario di Erdős (OpenAI 2026). A questo si affiancano i preprint, tutti dovuti a un modello interno OpenAI, di Alexeev, Putterman, Sawhney, Sellke e Valiant (2026a, 2026b) su una serie di problemi di Erdős in combinatoria, probabilità e teoria dei numeri, e il lavoro di Alexeev, Barreto, Li, Lichtman, Price, Shah, Tang e Tao (2026), che risolve il problema #1196 di Erdős–Sárközy–Szemerédi sui primitive sets introducendo un nuovo metodo (le catene di Markov con pesi di von Mangoldt) suggerito dall’output di GPT-5.4 Pro. Dall’altro lato, Google DeepMind ha pubblicato un paper, Advancing Mathematics Research with AI-Driven Formal Proof Search (Tsoukalas et al. 2026), in cui viene presentato AlphaProof Nexus e annunciata la soluzione formale di nove problemi di Erdős, oltre ad altre congetture in domini diversi (combinatoria additiva, ottica quantistica, teoria dei grafi, geometria algebrica, ottimizzazione convessa).
Ci sono molte conseguenze interessanti (oltre a quelle strettamente disciplinari) che da questi risultati si potrebbero trarre circa la natura degli LLM, del ragionamento in generale, e del rapporto tra ragionamento umano e artificiale. Ma voglio concentrami in questo articolo sul paper dei ricercatori di DeepMind perché da una fazione dei commentatori viene considerato come una evidenza a favore dei cosiddetti approcci neurosimbolici forti che a mio parere sono un testa-coda teorico sbagliato – su questo tema mi sono già intrattenuto in un precedente intervento sul Blog (Ciotti 2026). Il sistema presentato nel paper è molto complesso, con un’architettura che coinvolge Gemini, Lean, AlphaProof, meccanismi di validazione, la selezione di sketch promettenti tramite un punteggio Elo costruito da rater LLM, e naturalmente il lavoro preliminare e successivo degli esperti umani. Ma la questione interessante è da porsi, in relazione al punto di viste che vorrei argomentare è: chi o cosa svolge davvero il lavoro principale e produce la dimostrazione? Chi genera i candidati di passi di dimostraziomne, immagina la strategia, introduce lemmi intermedi, scompone un obiettivo troppo compatto in sotto-obiettivi più trattabili, decide quando chiamare uno strumento specializzato, riorienta il tentativo sulla base degli errori del proof checker?
La risposta, leggendo il workflow, mi pare abbastanza chiara, ed è una risposta che gli stessi autori del paper riconoscono con notevole chiarezza nella sezione di discussione finasle del paper. Il nucleo generativo del processo è il prover agent basato su un LLM. Il sistema riceve un file Lean con il teorema formalizzato e una conclusione “sorry” al posto della prova. A quel punto, l’agente modifica lo sketch, propone passaggi, introduce definizioni e lemmi ausiliari, prova strade diverse, consulta AlphaProof sui subgoal locali, integra i risultati e usa Lean come ambiente di controllo formale. Quando il verificatore Lean certifica che il passo è corretto, AlphaProof chiude porzioni della prova, ma è l’agente LLM a effettuare la ricerca nello spazio delle dimostrazioni. L’aspetto più rivelatore è questo: nell’analisi post-hoc condotta dagli autori, il basic agent, ossia la configurazione più semplice del sistema, tutti e nove i problemi di Erdős che il full-featured agent aveva risolto, con quest’ultimo che mantiene un vantaggio significativo solo sui problemi più difficili (segnatamente #125 e #138). Gli stessi autori riconoscono che l’efficacia del basic agent è stata sorprendente e attribuiscono il suo successo al lavoro svolto dal LLM supportato da quello che chiamano “the power of compiler feedback in grounding LLM reasoning”. Tutto il sofisticato impianto del full-featured agent non costituisce quindi il fattore decisivo: il fattore decisivo è la capacità generativa dell’LLM frontier più il filtro del compilatore: “Formal verification can serve as a filter for determining which proofs merit human review”.
Questa veloce disanima tecnica del sistema mi pare importante perché impatta direttamente sulle tesi di chi considera l’approccio di Deep Mind un chiaro caso di sistema neurosimbolico in senso forte. Infatti, credo che questa interpretazione sia a dir poco generosa, poiché è chiare che anche qui il formalismo svolge una funzione di verifica, una sorta di esoscheletro logico del processo di ragionamento. Senza LLM, questo sistema perderebbe la componente che esplora in modo produttivo lo spazio delle strategie dimostrative; tanto è vero che AlphaProof, eseguito in modalità standalone su tutti e nove i problemi, non ne risolve alcuno, e che le versioni del basic agent costruite su modelli più piccoli (Gemini 3.0 Flash, Gemini 3.1 Flash-Lite) falliscono anch’esse completamente, anche quando AlphaProof viene messo a loro disposizione come tool. Il fattore critico è dunque la combinazione tra LLM frontier e verifica formale. Va detto peraltro, per evitare semplificazioni, che AlphaProof non è un sistema simbolico classico in senso stretto: si tratta di una rete neurale simile a quelle già famose di DeepMind (da AlphaGo ad AlphaFold, che è valsa il Nobel a Demis Hassibis John Jumper) e addestrata via reinforcement learning a fare tree search su derivazioni espresse in Lean (Hubert et al. 2025). Quindi il contrasto rilevante non è tra “LLM” e “solver simbolico tradizionale”, bensì tra due paradigmi neurali differenti, uno aperto e generativo (il modello linguistico frontier che esplora liberamente lo spazio degli sketch), l’altro più strutturato e con interfaccia diretta al verificatore (la policy/value network di AlphaProof che cerca sequenze tattiche). Secondo i ricercatori di DeepMind la ricetta vincente è la combinazione dei due paradigmi neurali, ma è precisamente la componente aperta e generativa, quella tipica degli LLM frontier, a essere indispensabile per ottenere risultai di livello alto. Senza Lean, invece, il modello potrebbe ancora produrre idee, congetture, piani, analogie, decomposizioni, bozze di prova; perderebbe certo la possibilità di trasformare le dimostrazioni prodotte in prove formalmente certificati: ma, in fondo, non è esattamente ciò che avviene quando le prove vengono fatte da matematici umani? C’è anzi un dato del paper che vale la pena segnalare a sostegno proprio di questa simmetria: l’agente ha identificato alcune formalizzazioni errate nella letteratura, in particolare nei problemi #125 e #741(i), dove la nozione di “densità” risultava ambigua tra densità naturale, inferiore e superiore. Il sistema, cioè, non si limita a provare dentro un formalismo, ma riesce a segnalare attriti tra formalizzazione e contenuto matematico informale; e questa è un’attività che richiede precisamente quel tipo di esplorazione fluida di cui parlerò tra poco, e che un sistema puramente simbolico, ipoteticamente cieco rispetto al significato informale, non potrebbe in alcun modo svolgere.
Una mente, naturale o artificiale che sia, non può essere una macchina che manipola simboli formali secondo regole inferenziali esplicite. Le logiche formali, le notazioni matematiche, i calcoli, i diagrammi e i proof assistant sono tecnologie esterne del pensare: strumenti mediante i quali un sistema cognitivo consolida, controlla, comunica e rende verificabili pubblicamente i propri passaggi inferenziali. Un matematico umano non pensa “in Lean”; usa formalismi, scritture e tecniche di verifica per disciplinare una ricerca che nasce in uno spazio molto più fluido di analogie, intuizioni, schemi, tentativi, errori e riformulazioni. Naturalmente, i sistemi simbolici possono essere utili come scaffolding del pensiero quando il dominio è chiuso, formalizzato e computazionalmente trattabile. In matematica questa condizione può essere raggiunta, almeno in linea di principio, perché una dimostrazione può essere ricondotta a una sequenza di passi verificabili. Nei contesti aperti della comunicazione, dell’azione sociale e del senso comune, la situazione cambia radicalmente. E non potrebbe essere altrimenti, perché il vecchio frame problem (Pylyshyn 1987) mostra l’impossibilità, per sistemi logico-simbolici, di stabilire quali aspetti del mondo restano invariati, quali sono rilevanti, quali conseguenze devono essere tratte e quali invece devono essere ignorate in un ambiente aperto. Questo è un limite intrinseco dei sistemi che richiedono una formalizzazione completa e stabile del dominio. In ambito epistemologico, la conseguenza è che i modelli simbolici non possono funzionare come metodi di scoperta, ma solo, in casi ristretti e formalizzabili, come metodi di giustificazione (per usare la nota distinzione reichenbachiana tra contesto della scoperta e contesto della giustificazione).
Un modello connessionistico non esplora lo spazio delle ragioni applicando regole deduttive hard-coded su simboli discreti. Lo fa attraverso rappresentazioni distribuite e continue (che nei sistemi neurali artificiali sono codificate come vettori di numeri reali approssimati), che si trasformano lungo i vari strati del sistema e possono codificare non solo la continuazione immediata, ma anche vincoli futuri, candidati alternativi, stati intermedi e forme locali di pianificazione. La predizione del next token resta l’interfaccia esterna e l’obiettivo di addestramento fondamentale nel pre-training; non esaurisce, però, ciò che avviene nelle complesse fasi di fine tuning, e soprattutto ciò che accade internamente nel residual stream, dove il modello può costruire rappresentazioni orientate ai passaggi successivi e a configurazioni più globali del problema. Su questo punto, ormai, non si tratta più di pura speculazione teorica: i recenti lavori di interpretabilità meccanicistica mediante sparse autoencoder condotti nei laboratori di Anthropic hanno mostrato in modo empiricamente robusto sia l’esistenza di feature interpretabili semanticamente all’interno del residual stream dei modelli di produzione (Templeton et al. 2024), sia, attraverso le tecniche di attribution graph, la presenza di circuiti dedicati alla pianificazione anticipata: il modello, durante l’inferenza, costruisce attivamente rappresentazioni di token e obiettivi futuri prima di emetterli, e mostra forme di pianificazione in avanti e all’indietro nella generazione (Lindsey et al. 2025).
Questa cosa fatica a entrare nella testa di molti che guardano con scandalo e derisione agli LLM, e alle reti neurali in generale, con l’occhio dell’informatica teorica e ingegneristica del passato: quella che identifica i processi computazionali con algoritmi deterministici la cui esecuzione è controllabile a priori (almeno in linea di principio), strutture dati discrete, regole formali e inferenze deduttive perfettamente definite.
Riferimenti bibliografici
Alexeev, Boris, Kevin Barreto, Yanyang Li, Jared Duker Lichtman, Liam Price, Jibran Iqbal Shah, Quanyu Tang, e Terence Tao. 2026. «Primitive Sets and von Mangoldt Chains: Erdős Problem #1196 and Beyond». arXiv preprint arXiv:2605.00301.
Alexeev, Boris, Moe Putterman, Mehtaab Sawhney, Mark Sellke, e Gregory Valiant. 2026a. «Short Proofs in Combinatorics and Number Theory». arXiv preprint arXiv:2603.29961.
Alexeev, Boris, Moe Putterman, Mehtaab Sawhney, Mark Sellke, e Gregory Valiant. 2026b. «Short Proofs in Combinatorics, Probability and Number Theory II». arXiv preprint arXiv:2604.06609.
Hubert, Thomas, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žužić, Eric Wieser, Aja Huang, et al. 2025. «Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning». Nature, 1–3.
Lindsey, Jack, Wes Gurnee, Emmanuel Ameisen, Brian Chen, Adam Pearce, Nicholas L. Turner, Craig Citro, et al. 2025. «On the Biology of a Large Language Model». Transformer Circuits Thread. https://transformer-circuits.pub/2025/attribution-graphs/biology.html.
OpenAI. 2026. «An OpenAI Model Has Disproved a Central Conjecture in Discrete Geometry». OpenAI, 20 maggio 2026. https://openai.com/index/model-disproves-discrete-geometry-conjecture/.
Templeton, Adly, Tom Conerly, Jonathan Marcus, Jack Lindsey, Trenton Bricken, Brian Chen, Adam Pearce, et al. 2024. «Scaling Monosemanticity: Extracting Interpretable Features from Claude 3 Sonnet». Transformer Circuits Thread. https://transformer-circuits.pub/2024/scaling-monosemanticity/.
Tsoukalas, George, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, et al. 2026. «Advancing Mathematics Research with AI-Driven Formal Proof Search». arXiv preprint arXiv:2605.22763.
Pylyshyn, Zenon W., a c. di. 1987. The Robot’s dilemma: the frame problem in artificial intelligence. Theoretical issues in cognitive science. Ablex.
