Dieci risultati matematici con certificato Lean: cosa è verificabile

Intelligenza Artificiale

Consulenza EU AI Act: classificazione dei sistemi, policy, governance AI, formazione.

Scopri →

Ricerca e Sviluppo

Progetti di ricerca applicata su AI, imaging e robotica, con partner clinici e accademici.

Scopri →

Oggi, 1 agosto 2026, sono uscite due cose che parlano della stessa questione da due lati opposti. OpenAI ha pubblicato dieci risultati matematici ottenuti da un proprio modello, ognuno accompagnato da una dimostrazione formale che una macchina può ricontrollare. Qualche giorno prima Sam Altman ha detto in un podcast che siamo entrati nella singolarità.

Della prima affermazione si può fare qualcosa di concreto: scaricarla, eseguirla e vedere se il controllo passa. Per la seconda non c’è niente da eseguire.

Cosa ha pubblicato OpenAI

Il documento si chiama Ten Advances in Mathematics and Theoretical Computer Science, conta 249 pagine e raccoglie dieci risultati su problemi che, scrive OpenAI, non vedevano progressi sul risultato principale da almeno un decennio, in molti casi da molto di più. L’abstract attribuisce il lavoro a “un modello interno di OpenAI”, senza nominarlo.

Il nome compare altrove. Nei metadati del repository delle formalizzazioni, il file formalization.yaml dichiara metodo agent, modello Astra (OpenAI), framework Codex e un tempo di esecuzione di una settimana. Secondo quanto riportato dalla stampa specializzata, OpenAI indica un costo di calcolo complessivo di circa 2.000 dollari alle tariffe API di Sol per tutti e dieci i risultati, cifra che non comprende l’addestramento del modello né il lavoro umano di contorno.

I dieci risultati toccano geometria in alta dimensione, teoria dei codici, complessità dei circuiti aritmetici, teoria dei gruppi, algebre di von Neumann, complessità quantistica, crittografia reticolare e combinatoria estremale:

1. Impacchettamento di sfere in alta dimensione: determinata esattamente la forza asintotica del programma lineare di Cohn–Elkies
2. Codici binari e sferici: i limiti superiori classici migliorati di fattori esponenziali per tutti i parametri
3. Gruppi non sofici: costruito un gruppo non sofico esplicito, chiudendo la questione se ogni gruppo numerabile ammetta approssimazioni finite per permutazioni
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
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: cadono due congetture di teoria estremale dei grafi, i problemi 146 e 180 di Erdős

Che cosa garantisce un certificato Lean

Una dimostrazione scritta in Lean 4 viene ridotta a un termine di prova che il kernel del sistema controlla riga per riga contro l’enunciato dichiarato. Il kernel è piccolo, stabile e indipendente da chi ha scritto la dimostrazione. Se accetta, il teorema segue dagli assiomi della libreria, e non importa se a produrre il testo è stato un matematico, uno studente o un modello linguistico. La fiducia si sposta dal produttore al verificatore.

Restano tre cose che il kernel non controlla, e sono quelle da guardare.

Gli assiomi usati. Mathlib poggia su tre assiomi classici: propext, Classical.choice e Quot.sound. Se un file ne aggiunge altri con una dichiarazione axiom, sta assumendo qualcosa invece di dimostrarlo, e il comando #print axioms sul teorema principale lo rivela.

Le scorciatoie. Un sorry lasciato in un lemma fa passare tutto quello che ci sta sopra. Tattiche come native_decide delegano un pezzo di verifica al compilatore, allargando la base di codice di cui ci si fida.

La fedeltà dell’enunciato. Nessuna macchina chiude questo passaggio. 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 controlla una persona che legge. È il passaggio dove un errore non produce un fallimento rumoroso ma un teorema vero e inutile.

Cosa abbiamo controllato noi

Il repository è pubblico e i controlli costano pochi minuti, quindi li abbiamo eseguiti. Sono 550.000 righe di Lean distribuite su 23 file, contro leanprover/lean4:v4.32.0 e Mathlib alla stessa revisione.

Sui dieci certificati principali: zero sorry, zero dichiarazioni axiom, zero occorrenze di native_decide. Le uniche 42 occorrenze di sorry stanno tutte nella cartella ComparatorChallenges, che non contiene le dimostrazioni ma le sfide predisposte per farle ricontrollare da un kernel indipendente, Comparator, attraverso lean4export e l’implementazione alternativa nanoda_bin. Un sorry lì dentro è l’enunciato lasciato aperto per il verificatore terzo, e non un buco nella dimostrazione.

Il file formalization.yaml chiude il cerchio sulla fedeltà dell’enunciato: elenca dodici risultati principali con il nome esatto della dichiarazione Lean da guardare, il file che la contiene e gli assiomi usati, che sono i tre standard e nessun altro. Per il gruppo non sofico, per dire, il nome è SoficGroups.SourceTopLevelCompressionFinal.exists_finitelyPresented_nonsofic_group. Il lavoro umano di controllo passa così da 249 pagine a dodici enunciati da leggere.

Due precisazioni sul valore di quanto sopra. La prima: abbiamo verificato l’assenza di scorciatoie nel sorgente, non l’accettazione da parte del kernel, che richiede la toolchain e un tempo di compilazione lungo. Chi vuole farlo trova le istruzioni nel README, sono lake exe cache get e lake build All. La seconda, che vale più di tutte le altre: nello stesso file di metadati il campo review dichiara status: agent-reviewed. La revisione dichiarata è quella di un agente, non di un revisore umano né di una rivista.

Sul fronte dell’attribuzione il repository dichiara il lavoro precedente su cui si appoggia, i due progetti Sphere-Packing-Lean, con author_contacted: yes e un ringraziamento esplicito. E il capitolo su Connes annota di aver saputo, durante la preparazione, di un lavoro indipendente e concorrente di Shuoxing Zhou, anch’esso un controesempio alla congettura, sviluppato in parte con l’assistenza di GPT-5.6 Sol.

Il precedente di maggio

Non è il primo colpo. Il 20 maggio 2026 un modello interno di OpenAI aveva risolto il problema delle distanze unitarie nel piano, posto da Erdős nel 1946, trovando una famiglia infinita di costruzioni con n^(1+δ) coppie a distanza unitaria per un δ fisso, poi precisato in δ = 0,014 da Will Sawin.

Quella volta la verifica fu umana e organizzata: OpenAI mandò la dimostrazione in privato a matematici indipendenti, che produssero un articolo di accompagnamento di 19 pagine firmato da nove ricercatori, fra cui Noga Alon, Thomas Bloom, Tim Gowers, Daniel Litt, Sawin, Jacob Tsimerman e Melanie Matchett Wood. Gowers parlò di “a milestone in AI mathematics”, Alon di “an outstanding achievement”.

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 costa molto meno per ogni risultato successivo.

La dichiarazione di Leiden

Il contesto in cui l’annuncio arriva non è neutro. A giugno 2026 un gruppo internazionale di matematici ha pubblicato la dichiarazione di Leiden su intelligenza artificiale e matematica, nata da un workshop del settembre 2025 al Lorentz Center dell’Università di Leida e sostenuta dall’Unione Matematica Internazionale, con firme fra cui Terence Tao, Peter Scholze, Kevin Buzzard e Scott Aaronson.

Elenca cinque rischi:

• risultati inaffidabili, perché una dimostrazione può sembrare convincente e contenere un errore quasi invisibile
• attribuzione mancante, con modelli che producono risultati senza citare il lavoro umano su cui si appoggiano
• dipendenza e disuguaglianza rispetto a sistemi proprietari chiusi e a risorse di calcolo costose
• incentivi distorti, con risultati comunicati tramite comunicati stampa e blog invece che riviste con revisione fra pari
• perdita di autonomia della ricerca, se le domande vengono scelte perché automatizzabili invece che perché ritenute profonde

L’annuncio di oggi risponde bene al primo e al secondo rischio, con il certificato e con le citazioni del lavoro precedente. Sul terzo e sul quarto sta esattamente dove la dichiarazione teme: il modello è chiuso e interno, e il canale è una pagina aziendale con un PDF.

Altman e la parola singolarità

Nel fine settimana del 28 luglio 2026, al podcast Relentless, Sam Altman ha detto: “We are now, like, in the singularity.” Non è una posizione nuova per lui: nel saggio The Gentle Singularity del giugno 2025 aveva scritto “We are past the event horizon; the takeoff has started”, con la cautela che “questo non è la stessa cosa di un sistema AI che aggiorna il proprio codice in modo completamente autonomo, ma è comunque una versione larvale dell’auto-miglioramento ricorsivo”.

La parola ha però un significato tecnico che ha sessant’anni e una soglia verificabile: un sistema che migliora il proprio successore senza direzione umana. È un evento discreto, che si può testare. Quello che Altman descrive è uno stato percettivo, il senso di meraviglia che diventa abitudine, e uno stato percettivo non si misura allo stesso modo.

I dati che si citano a sostegno raccontano una crescita reale e una cosa diversa dalla soglia. Gli intervalli fra rilasci di modelli di frontiera si sono compressi a circa 60 giorni nel 2026, contro 315 e 195 giorni in precedenza per Anthropic e OpenAI. Anthropic ha dichiarato a maggio 2026 che oltre l’80% del codice che entra nella propria codebase di produzione è scritto da Claude. Le misure METR sull’orizzonte temporale dei compiti, come riportate da Forbes, passano da circa quattro minuti nel marzo 2024 a novanta minuti un anno dopo e a dodici ore all’inizio del 2026.

Rilasciare più in fretta è un’altra cosa dal migliorare più in fretta, e nessuno di questi numeri misura un sistema che migliora il proprio successore da solo. Lo dice anche chi sta dentro: secondo la stessa ricostruzione, il capo della ricerca di OpenAI Jakub Pachocki non si aspetta entro fine anno sistemi capaci di migliorare autonomamente la propria architettura, e Altman colloca il collo di bottiglia nell’infrastruttura fisica, cioè data center, energia e permessi, più che negli algoritmi.

Cosa ne pensiamo

Sul merito matematico non siamo qualificati a esprimerci. I matematici che lavorano su queste congetture non hanno ancora avuto il tempo di attraversare gli argomenti con la profondità che di solito richiedono, quindi al momento nessun giudizio esterno sul contenuto è consolidato. Quello su cui possiamo dire qualcosa è il meccanismo di garanzia, perché è lo stesso problema che affrontiamo quando un cliente ci chiede se può fidarsi di un sistema.

Quello che conta qui è che l’affermazione arriva insieme all’oggetto che permette di smentirla. Un certificato Lean è un artefatto ostile a chi lo produce: se la dimostrazione non regge, il kernel dice no, e lo dice a chiunque lo esegua, non solo a chi ha accesso al modello. Questo è il contrario di un benchmark autodichiarato, ed è la ragione per cui i due annunci di questa settimana non stanno sullo stesso piano.

Da qui tre osservazioni che valgono fuori dalla matematica.

Una verifica indipendente vale quanto è piccola la base di fiducia. Il kernel di Lean funziona perché è minuscolo e ricontrollabile, tanto che si può passare il termine di prova a un’implementazione alternativa del kernel e vedere se anche quella accetta. Nei sistemi che costruiamo l’equivalente è tenere il punto di controllo separato dal componente che produce l’effetto, che è il criterio con cui mettiamo la governance dentro il ciclo e non accanto, come descriviamo in Open Intelligence, Secure Governance e nel paradigma OISG.

La traduzione dell’enunciato è il punto dove si perde, ed è umana. Il kernel dimostra quello che gli si chiede di dimostrare. Se l’enunciato formale non è la domanda che interessa, il risultato è corretto e irrilevante, e nessun controllo automatico lo segnala. È la stessa asimmetria che troviamo negli audit di conformità: un requisito tradotto male produce evidenza perfetta di una cosa che non serve. Per questo il campo formalization.yaml che elenca dichiarazione per dichiarazione ci sembra la parte più utile del rilascio, molto più della cifra sul costo.

agent-reviewed è un dato di stato, non un difetto nascosto. OpenAI lo ha scritto nei propri metadati, ed è corretto che ci sia. Dice però con precisione a che punto della catena siamo: la revisione fra pari deve ancora cominciare, e la dichiarazione di Leiden è stata firmata a giugno proprio per il rischio che il comunicato prenda il posto di quel passaggio. Le due cose convivono senza contraddirsi, purché non si legga il certificato come se fosse anche la revisione.

Per chi costruisce software la lezione trasferibile è concreta e la conosciamo già in un’altra forma. Un’affermazione che porta con sé l’artefatto per controllarla vale più di una affermazione più forte senza. È lo stesso principio per cui un SBOM conta più di una dichiarazione di sicurezza, e la scadenza di dicembre 2027 del Cyber Resilience Act chiede esattamente quello: non la promessa che i componenti siano a posto, ma l’inventario che permette di verificarlo.

Sulla singolarità la nostra posizione è che la parola, usata come la usa Altman, non è controllabile e quindi non è utile per decidere niente. La domanda operativa per chi progetta sistemi resta quella di sempre e ha una risposta misurabile: cosa fa il sistema senza che nessuno gliel’abbia chiesto, e cosa lascia dietro di sé perché qualcun altro possa controllarlo.

Fonti

• OpenAI: Ten advances in mathematics and theoretical computer science
• Il manoscritto, 249 pagine (PDF)
• openai/ten-proofs: i certificati Lean 4 su GitHub
• Comparator, il verificatore indipendente del kernel Lean
• Leiden Declaration on Artificial Intelligence and Mathematics
• Università di Leida: la dichiarazione avverte che l’AI mette alla prova i valori fondamentali della matematica
• The Next Web: OpenAI says its next model, Astra, has solved ten open problems in mathematics
• Forbes: Sam Altman Says We’re In The Singularity. What Does He Actually Mean?