Il 1 agosto 2026 OpenAI ha pubblicato Ten Advances in Mathematics and Theoretical Computer Science, 249 pagine con dieci risultati di matematica e informatica teorica ottenuti da un proprio modello, e insieme un repository con una dimostrazione formale in Lean 4 per ciascuno dei risultati principali, che una macchina può ricontrollare. Sui risultati non ho titolo per dire nulla. Sul meccanismo di garanzia qualcosa si può dire, e la settimana in cui l’annuncio arriva rende la domanda meno teorica del solito: il 28 luglio Lean ha rilasciato una patch per un bug di solidità del proprio kernel.

Cosa contiene il rilascio

L’abstract attribuisce il lavoro a «an internal OpenAI model»; la pagina di annuncio lo nomina, una versione interna di Astra. I metadati del repository indicano framework Codex e un tempo di esecuzione di una settimana. OpenAI dichiara un costo di circa 2.000 dollari alle tariffe API di Sol per tutti e dieci i risultati — cifra che copre i soli token necessari a trovare le soluzioni, non l’addestramento del modello né la preparazione dei manoscritti e la formalizzazione, che l’azienda dichiara come lavoro proprio.

I dieci capitoli, negli enunciati dell’abstract:

  1. Impacchettamento di sfere. Determinata esattamente la forza asintotica del programma lineare di Cohn–Elkies.
  2. Codici binari e sferici. I limiti superiori classici per i codici binari e sferici a distanza fissata migliorati di fattori esponenziali per tutti i parametri.
  3. Gruppi non sofici. Costruito un gruppo non sofico esplicito, e la questione se ogni gruppo numerabile ammetta approssimazioni finite per permutazioni si chiude.
  4. Congettura di rigidità di Connes. Costruiti infiniti gruppi con proprietà (T) a due a due non isomorfi con la stessa algebra di von Neumann, e la congettura cade.
  5. Complessità dei circuiti aritmetici. Per il permanente, i circuiti senza divisione richiedono Ω(n² log log n) porte e le formule Ω(n⁴ / log n) foglie.
  6. Ripetizione parallela quantistica. Dimostrata la ripetizione parallela esponenziale per ogni gioco entangled finito a due giocatori.
  7. Closest vector problem. Una riduzione diretta da 3SAT dà hardness a fattore n^(1/400).
  8. Congettura del volume di Ehrhart. Dimostrato il limite netto (n+1)ⁿ/n! in ogni dimensione, per i corpi convessi il cui baricentro è il loro unico punto reticolare interno.
  9. Numeri di Ramsey multicolore. Un limite inferiore superesponenziale prova R_k(3) = k^Θ(k), che è il problema 183 di Erdős.
  10. Compattezza e degenerazione. Due costruzioni bipartite smentiscono la congettura di compattezza di Erdős e Simonovits e una congettura di degenerazione di Erdős.

Che cosa garantisce il kernel

Una dimostrazione scritta in Lean viene ridotta a un termine di prova che il kernel del sistema controlla contro l’enunciato dichiarato. Il kernel è piccolo e indipendente da chi ha scritto la dimostrazione: le tattiche, i metaprogrammi e l’elaboratore stanno fuori dalla base fidata, perché qualunque cosa producano deve poi superare quel controllo. Se il kernel accetta, il teorema segue dagli assiomi della libreria, e non fa differenza se a produrre il testo è stato un matematico, uno studente o un modello linguistico. È il criterio di de Bruijn, e sposta la fiducia da chi produce l’affermazione a chi la controlla. È quello che distingue un rilascio del genere da un benchmark autodichiarato.

Ci sono quattro cose che il kernel non copre.

Gli assiomi. Mathlib aggiunge tre assiomi alla teoria dei tipi di Lean: propext, Classical.choice e Quot.sound. Solo il secondo è propriamente classico, gli altri due riguardano estensionalità e quozienti e sono accettati anche in matematica costruttiva. Se un file ne aggiunge altri con una dichiarazione axiom, sta assumendo qualcosa invece di dimostrarlo, e il comando #print axioms sul teorema lo rivela.

Le scorciatoie. Un sorry lasciato in un lemma fa passare tutto quello che ci sta sopra, e lo fa quasi in silenzio: Lean emette l’avviso declaration uses 'sorry' solo sulla dichiarazione che contiene il sorry, non su quelle che la usano. A valle lo rivela #print axioms, che riporta sorryAx, ed è un valore da leggere, non un errore che blocca la build.

Con una tattica come native_decide il kernel non verifica il calcolo delegato: accetta un assioma che ne asserisce il risultato, e la base fidata si allarga al generatore di codice, al runtime e a ogni definizione marcata @[implemented_by] o @[extern], che i verificatori esterni non possono rivalidare. Una traccia negli assiomi c’è sempre stata — fino alla 4.28.0 il solo Lean.trustCompiler, dalla 4.29.0 un assioma dedicato per ogni singola computazione, controllabile una per una.

La fedeltà dell’enunciato. Il kernel garantisce che la dimostrazione dimostri l’enunciato scritto in Lean. Che quell’enunciato sia la congettura di cui parla il titolo è una traduzione, e la traduzione la legge una persona. È il passaggio dove un errore non lascia traccia da nessuna parte e produce un teorema vero e fuori bersaglio. Nel rilascio ce n’è un esempio leggibile: il capitolo sui gruppi non sofici dice che «an explicit non-sofic group is constructed», mentre l’enunciato Lean è un’esistenza, ∃ (G : Type) (_ : Group G), Group.IsFinitelyPresented G ∧ ¬ Sofic G. Chi controlla deve anche leggere la definizione di Sofic, che è scritta nel file di sfida e non presa da Mathlib.

Quello che resta dopo il sì. La solidità logica di Lean non è dimostrabile dentro Lean; l’infrastruttura che esegue il controllo deve non essere compromessa; nessun difetto di implementazione deve colpire tutti i verificatori insieme. Il manuale lo elenca per esteso, e vale la pena leggerlo prima di dire che un certificato chiude la questione.

Il verificatore è software

Il 28 luglio 2026 Lean ha rilasciato la 4.32.2, un rilascio di sola correzione. Le note dicono: «This point release fixes a soundness bug in the kernel. The issue was discovered by Ramana Kumar and reported by Kiran Gopinathan. A malicious meta program can trick the kernel into accepting a proof of False, or any other theorem. The kernel’s handling of nested inductive types with phantom type parameters was incomplete and bypassed the type checker.» Il trattamento incompleto dei tipi induttivi annidati con parametri fantasma aggirava il type checker, e le note aggiungono che il difetto era sfruttabile anche passando per Comparator.

Il repository di OpenAI fissa leanprover/lean4:v4.32.0 nel lean-toolchain e la stessa revisione per Comparator, cioè versioni anteriori alla patch. Questo non è un motivo per dubitare di queste dieci dimostrazioni: l’exploit richiede un metaprogramma ostile e nei dieci file principali non c’è metaprogrammazione — niente unsafe, niente meta def, niente @[implemented_by]. È però la misura di che tipo di garanzia sia. Il confine è un programma, e vale finché non emerge il difetto giusto nel punto giusto — lo stesso ragionamento che si fa sulle sandbox che dovrebbero contenere un agente. La differenza a favore del certificato è che qui il difetto è stato trovato, pubblicato con numero di issue e corretto in giornata, e chiunque può rieseguire il controllo su una versione aggiornata.

Cosa si può ricontrollare

Il file formalization.yaml elenca dodici dichiarazioni principali con il nome esatto, il file che le contiene e gli assiomi usati. Dodici e non dieci perché due capitoli ne portano due ciascuno. Chi vuole controllare la traduzione ha dodici enunciati da leggere invece di 249 pagine.

Alcune cose vanno dette con precisione, perché il rilascio è più sfumato di come lo si racconta.

  • Le 249 pagine non nominano mai Lean. L’accoppiamento fra ciascun risultato e il suo certificato è affermato dal repository, non dal manoscritto.
  • I certificati coprono i risultati principali, non ogni enunciato del documento. Il capitolo sui circuiti aritmetici annuncia due limiti e solo quello sulle formule ha una dichiarazione Lean.
  • Comparator è il giudice sandboxato della Lean FRO: compila la soluzione isolata, ne esporta l’ambiente e controlla che i teoremi dimostrino l’enunciato del file di sfida e non usino assiomi fuori dalla lista permessa. Il kernel indipendente che affianca quello di Lean è un altro programma, nanoda, scritto in Rust, e tutti i dodici file di configurazione lo attivano.
  • La sfida sul closest vector problem usa i definition holes di Comparator, per i quali il controllo automatico verifica solo che nome, tipo e livelli di universo coincidano. Il README di Comparator avverte che quelle soluzioni vanno sempre controllate da un verificatore ulteriore, eventualmente umano. La garanzia formale su quel risultato è più debole che sugli altri undici.
  • I dieci file principali non contengono sorry, dichiarazioni axiom né valutazione nativa: si verifica con un grep sul clone, tenendo presente che i file sotto ComparatorChallenges/ i sorry li contengono per costruzione, perché una sfida è appunto un enunciato senza dimostrazione.
  • Nello stesso file il campo review dichiara status: agent-reviewed, e a oggi non risulta pubblicamente che qualcuno abbia eseguito Comparator su questi file. La revisione fra pari deve ancora cominciare.

Il precedente di maggio

Il 20 maggio 2026 un modello interno di OpenAI aveva smentito una congettura di Erdős del 1946 sulle distanze unitarie nel piano, costruendo insiemi di n punti con n^(1+δ) coppie a distanza unitaria per un δ fisso, con il valore esplicito 0,014 fissato lo stesso giorno da Will Sawin, in un lavoro già citato nell’annuncio. Il problema resta aperto — l’esponente vero sta ora fra n^1,014 e il limite superiore O(n^(4/3)) di Spencer, Szemerédi e Trotter — ma la congettura che il limite fosse n^(1+o(1)) è caduta. Per ottant’anni il miglior limite inferiore era la griglia √n × √n di Erdős stesso, con crescita sub-polinomiale nell’esponente. Passare a un δ fisso è un salto di natura diversa da un miglioramento numerico, e il metodo è di teoria dei numeri, non di combinatoria, che è probabilmente il motivo per cui in geometria discreta non l’aveva trovato nessuno.

Quella volta la verifica fu umana e organizzata: OpenAI mandò la dimostrazione in privato a matematici indipendenti, che pubblicarono un articolo di accompagnamento di 19 pagine firmato da nove ricercatori, fra cui Noga Alon, Thomas Bloom, Tim Gowers, Daniel Litt, Jacob Tsimerman e Melanie Matchett Wood. Gowers vi scrisse «a milestone in AI mathematics», Alon «an outstanding achievement». Le due frasi circolano da sole, e l’articolo che le contiene è più diviso di così. È Bloom a scrivere che forse qualcuno nel settore resterà un po’ deluso da quanto poco il risultato dica, e che la dimostrazione originale, pur del tutto valida, «was significantly improved by the human researchers at OpenAI» e dagli altri matematici coinvolti nel lavoro.

Fra maggio e agosto è cambiato il modo di garantire il risultato, da un gruppo di esperti che legge a un certificato che si ricontrolla da solo. Le due strade non si escludono, e la seconda ha una proprietà che la prima non ha: chiunque può rifarla, quante volte serve, senza chiedere di nuovo tempo a un matematico.

La dichiarazione di Leiden

Il 2 giugno 2026 un gruppo di lavoro di sedici persone da quindici istituzioni ha pubblicato la dichiarazione di Leiden su intelligenza artificiale e matematica, nata dal workshop Mechanization and Mathematical Research tenuto al Lorentz Center di Leida nel settembre 2025 e poi sostenuta dall’Unione Matematica Internazionale. Fra i firmatari ci sono Terence Tao, Peter Scholze, Kevin Buzzard e Scott Aaronson. Elenca cinque minacce:

  • Correttezza. Argomenti plausibili ma inaffidabili, difficili da distinguere da dimostrazioni corrette. Vale anche per le formalizzazioni, dove la difficoltà sta nella traduzione fra i concetti codificati per la macchina e quelli presentati agli umani.
  • Attribuzione. Modelli che non citano i lavori umani che sintetizzano, e dati raccolti sfruttando accordi di licenza pensati per altro o violando il copyright.
  • Incentivi. L’uso dell’AI premiato per sé stesso in assunzioni, finanziamenti e riconoscimenti, a svantaggio di chi non vi ha accesso o non vuole usare tecnologie controllate da organizzazioni di cui non condivide i valori.
  • Valutazione. Risultati comunicati da canali informali come comunicati stampa e post di blog, su tempi di mercato e prima che la comunità matematica possa applicare i propri processi.
  • Autonomia. Domande di ricerca scelte perché automatizzabili invece che per il giudizio esperto sulla loro profondità.

Il passaggio che descrive meglio l’annuncio di agosto sta però nelle raccomandazioni all’industria. La matematica è attraente per chi costruisce modelli generalisti perché «the correctness of formalized proofs can be checked automatically, without the need for human oversight», il che fornisce un segnale di addestramento praticamente illimitato, nell’assunto che la capacità sviluppata sul theorem proving si estenda al ragionamento generale. Il certificato Lean è insieme la risposta alla prima minaccia dell’elenco e la ragione industriale per cui questi risultati esistono. L’avvertimento contro l’uso di compiti matematici specifici come metrica delle capacità di ragionamento generale di un prodotto commerciale sta invece fra le minacce, alla quarta voce, e colpisce l’annuncio in pieno.

La dichiarazione non è un consenso unanime. Il 26 luglio Gowers ha spiegato di aver partecipato al workshop e di non aver firmato, perché in più punti la dichiarazione fa affermazioni e raccomandazioni su cui si sente incerto: gli sembra problematica la nozione stessa di valutazione appropriata, dato che matematici diversi danno giudizi molto diversi senza che nessuno abbia torto, e alcune parti gli paiono orientate a preservare lo stato attuale delle cose. Conclude comunque che il documento è un contributo importante. È lo stesso genere di documento del framework proposto da Hassabis a luglio, e va letto con lo stesso criterio: cosa dichiara in termini osservabili e cosa resta un principio.

La parola singolarità

Al podcast Relentless del 25 luglio 2026 Sam Altman ha detto «this is the most interesting important thing I can imagine doing, and we are now like in the singularity». Non è una posizione nuova per lui: nel saggio The Gentle Singularity del 10 giugno 2025 aveva scritto «We are past the event horizon; the takeoff has started», con la cautela che «of course this isn’t the same thing as an AI system completely autonomously updating its own code, but nevertheless this is a larval version of recursive self-improvement».

La parola ha una storia meno compatta di come viene usata. Nel 1965 I.J. Good descrive l’intelligence explosion, cioè una macchina che progetta macchine migliori di sé, e quella è una soglia in principio osservabile. La singolarità di Vernor Vinge, codificata nel 1993, è definita al contrario come il punto oltre il quale la capacità di prevedere il futuro si rompe, e per costruzione non è verificabile. Le due cose vengono usate come se fossero la stessa.

I numeri che si citano a sostegno descrivono una crescita reale, e conviene prenderli alla fonte. L’Anthropic Institute scrive che a maggio 2026 oltre l’80% del codice integrato nella codebase di Anthropic era scritto da Claude, precisando in nota che la metrica è la quota di righe fuse in produzione e sostenendo nello stesso documento che questo non è ancora auto-miglioramento ricorsivo, perché gli obiettivi, l’architettura e la revisione restano umani — una distinzione che regge finché la verifica ha strumenti all’altezza. METR pubblica il dato grezzo del proprio orizzonte temporale al 50% di successo: 3,95 minuti per Claude 3 Opus nel marzo 2024, 60,4 minuti per Claude 3.7 Sonnet un anno dopo, 718,8 minuti — poco meno di dodici ore — per Claude Opus 4.6 nel febbraio 2026, con un intervallo di confidenza fra 5,3 e 60,6 ore e l’avvertenza che sopra le sedici ore le misure non sono affidabili con la suite attuale. Il tempo di raddoppio dichiarato è di 128,7 giorni considerando i modelli dal 2023 in poi.

Nessuno di questi numeri misura un sistema che progetta il proprio successore da solo. Lo stesso Altman colloca il collo di bottiglia nell’infrastruttura fisica: «There is relatively too much focus on algorithms that create better algorithms and not enough focus on data centers that can create more data centers».

Tempi di mercato

L’8 giugno 2026 OpenAI ha annunciato di aver depositato una S-1 riservata alla SEC, scrivendo «we expect it to leak so we’re just announcing it» e che i tempi non sono decisi, «it may be a while because there are things we want to do that are likely easier as a private company». Il documento non è pubblico, perché una registrazione riservata compare su EDGAR solo quando viene depositata in chiaro. Il 9 luglio, alla domanda se la quotazione arrivi entro l’anno, Altman ha risposto «I don’t know»; il 1 giugno l’aveva definita «a financing event». Lo stesso giorno Anthropic aveva annunciato di aver depositato a sua volta una S-1 riservata. Entrambi i laboratori sono avviati alla quotazione, ed è di pubblico dominio.

Che tutto questo pesi sul modo in cui la ricerca viene comunicata lo scrive la dichiarazione di Leiden, senza nominare aziende. La quarta minaccia parla di pubblicità cercata «on market timelines», prima che i processi di valutazione della comunità possano svolgersi. Ai decisori politici raccomanda di non fermarsi ai comunicati, perché «there is currently a strong commercial incentive on the part of the technology industry to overstate the capabilities of their products». La quinta minaccia porta lo stesso effetto dentro l’università: con i bilanci sotto pressione gli incentivi professionali spingono i ricercatori a collaborare con le aziende tecnologiche «on asymmetric terms», e a quel punto la distorsione tocca la ricerca e non solo il mercato. Fuori dalla matematica la pressione si misura: il 9 luglio S&P ha declassato Oracle a BBB-, un gradino sopra il livello speculativo, citando la concentrazione dei propri obblighi contrattuali residui su un solo cliente, che è OpenAI.

Su questo annuncio non ho niente da portare. Nessuna fonte collega il rilascio del 1 agosto a un evento finanziario, e sul criterio della dichiarazione il caso va anzi nella direzione opposta, perché è arrivato con un manoscritto e con certificati che chiunque può rieseguire invece che con un comunicato senza divulgazione. La struttura però non cambia per un caso in controtendenza, e dovremo abituarci a leggere notizie di questo tipo, sempre più spesso e con sempre meno tempo fra l’annuncio e il momento in cui qualcuno lo valuta davvero. L’unica cosa che vedo funzionare è quella di cui parla tutto l’articolo, dentro e fuori la matematica: chiedere per prima cosa cosa arriva allegato che permetta di controllare.

Immagine di copertina: P. Oxy. I 29, frammento degli Elementi di Euclide con il diagramma della Proposizione II.5, I-II secolo d.C. — University of Pennsylvania, pubblico dominio — https://commons.wikimedia.org/wiki/File:P._Oxy._I_29.jpg