OpenAI, dieci risultati matematici formalizzati in Lean: il ruolo del modello interno

Il 1° agosto OpenAI ha pubblicato il manoscritto "Ten Advances in Mathematics and Theoretical Computer Science", attribuendo i risultati a un proprio modello interno. Contestualmente è stato creato il repository GitHub `openai/ten-proofs`, che rende disponibili le formalizzazioni Lean 4 delle dieci dimostrazioni. Tra i risultati spiccano il miglioramento dell'esponente per l'impacchettamento di sfere — il primo dal 1978 —, la costruzione di un gruppo non-sofico e un controesempio alla congettura di rigidità di Connes. Il repository è un progetto Lean 4.32.0 basato su mathlib, pubblicato con licenza Apache-2.0: chiunque può ricompilare le dimostrazioni con `lake exe cache get` e `lake build All`, e una cartella ComparatorChallenges spiega come fare la verifica in modo indipendente.

Le cronache hanno collegato questi risultati ad "Astra", il nome della prossima famiglia di modelli annunciata da OpenAI lo stesso 1° agosto; il manoscritto però parla solo di "un modello interno", non rilasciato. Dati come il costo di circa 2.000 dollari in token o le 249 pagine del documento provengono da cronache di terze parti, in quanto la pagina di annuncio ufficiale è attualmente inaccessibile. Il paper include ringraziamenti a matematici umani per la rilettura e segnala un lavoro indipendente e concomitante di Shuoxing Zhou, sviluppato in parte con l'assistenza di GPT-5.6 Sol.

Secondo SiliconANGLE gli argomenti matematici provengono dal modello, ma sono stati ricercatori umani a trasformarne l'output in manoscritti pubblicabili: quanto pesi quella rifinitura non è quantificato. L'uso di Lean 4 sposta il dibattito: se il certificato garantisce la validità logica della dimostrazione, non conferma automaticamente che l'enunciato formalizzato coincida con il problema aperto storico, controllo che resta di competenza umana. Nessuno dei dieci risultati ha superato una peer review formale. Il precedente pesa: nell'ottobre 2025 l'annuncio di dieci problemi di Erdős "risolti" da GPT-5 si rivelò infondato e Thomas Bloom, curatore di erdosproblems.com, lo definì una grave rappresentazione errata. Sui dieci risultati di oggi lo stesso Bloom parla invece di "big news". Come osserva il fisico teorico Tobias J. Osborne, i 2.000 dollari citati rappresentano il costo dei token vincenti, non il "raccolto" totale dei tentativi, un dato su cui OpenAI non ha fornito informazioni. Questo scenario si inserisce nel contesto della "Leiden Declaration on Artificial Intelligence and Mathematics", pubblicata a giugno 2026 e sostenuta secondo the-decoder da oltre 3.000 matematici e dall'International Mathematical Union, che chiede trasparenza, tutela dei diritti degli autori e responsabilità umana sui risultati.

La vera notizia non è che una macchina ha fatto matematica — accade da mesi — ma che stavolta ogni risultato arriva con un certificato Lean ricompilabile: per giudicare non serve fidarsi di chi annuncia. Tuttavia, finché il rapporto tra tentativi falliti e successi rimarrà un segreto industriale, la valutazione dell'efficienza di questi modelli resterà un esercizio di fede più che di statistica.