In quella che può essere descritta solo come l'equivalente accademico di far cadere un pianoforte sulla testa di qualcuno e poi chiedergli di recensire lo spartito, OpenAI ha rilasciato questa settimana quasi 400 risultati matematici generati dall'IA, distribuiti su più di 700 manoscritti. La reazione della comunità matematica è variata da "sbalorditivo" a "pura follia" - e questi erano quelli educati.

La raccolta spazia dalla combinatoria, a diversi rami della geometria, teoria dei numeri, informatica teorica, algebra, topologia, probabilità e meccanica statistica, e fisica matematica. È così vasta che OpenAI si è sentita in dovere di pubblicare una guida su come navigare lo sterminato repository GitHub, il che è un po' come consegnare a qualcuno una mappa di un edificio che hai appena dato alle fiamme.

"Solo scorrere l'intero elenco degli abstract è opprimente", ha detto Álvaro Lozano-Robledo, professore di matematica all'Università del Connecticut. Diversi matematici hanno detto a The Verge che semplicemente esaminare l'indice e gli abstract di circa 40 pagine ha richiesto loro quasi un'ora. Per chi tiene il punteggio a casa, un'ora solo per leggere il menu.

Sparsi tra le centinaia di manoscritti ci sono formalizzazioni in Lean, un linguaggio di programmazione e assistente di dimostrazione che consente di verificare i risultati computazionalmente. Queste formalizzazioni si sono dimostrate strumentali nel valutare alcune precedenti affermazioni matematiche di OpenAI, dando ai ricercatori la fiducia che un'affermazione sia logicamente corretta anche se non comprendono appieno l'argomentazione alla base - il che è un po' come fidarsi di una calcolatrice senza sapere cosa sia la divisione.

Ma il grado di verifica di ciascun risultato variava enormemente. Su GitHub, OpenAI ha riconosciuto che i risultati sono "in diverse fasi di verifica" e che "molti, ma non tutti, i manoscritti sono stati formalizzati". Al momento in cui scriviamo, meno della metà dei manoscritti nella raccolta sembra essere stata descritta formalmente. OpenAI ha affermato che solo 300 risultati principali su 719 manoscritti erano stati formalizzati - circa il 42% - e che "aggiornerà il repository con ulteriori formalizzazioni man mano che le otterremo". Quindi, circa il 58% dell'apocalisse matematica rimane non verificato. Dormite sonni tranquilli.

Diversi matematici si sono lamentati con The Verge della mancanza di formalizzazione, in particolare dato l'enorme numero di risultati. Anche quando il codice Lean accompagna un risultato, la valutazione non è istantanea. I ricercatori devono verificare che la formalizzazione dimostri effettivamente ciò che il risultato afferma - un altro processo che richiede tempo. Diversi studiosi che hanno esaminato gli articoli hanno detto che anche dove erano fornite dimostrazioni verificabili al computer, la qualità era incoerente e le affermazioni verificate non sempre sembravano corrispondere accuratamente alle affermazioni nei manoscritti di accompagnamento.

Kevin Buzzard, professore di matematica all'Imperial College di Londra, ha detto di aver identificato numerosi teoremi nel suo campo di lavoro - teoria algebrica dei numeri - di cui solo circa sei si sono immediatamente "distinti". Pochi, se non nessuno, di questi sembravano essere formalmente verificati in Lean. "Quindi, o devo leggere slop probabilmente non corretto, o aspettare che altri facciano lo stesso, o aspettare che qualcuno li formalizzi prima di poter dire con certezza che i risultati siano anche solo corretti". Le preoccupazioni di Buzzard sono state echeggiate da numerosi altri ricercatori, che presumibilmente avevano altre cose da fare questa settimana.

Buzzard era lungi dall'essere solo nel preoccuparsi dello "slop" dell'IA - una scorciatoia per materiale generato dall'IA di bassa qualità e spesso erroneo che compare sempre più online e nel mondo reale, inclusi articoli accademici. Come in altri campi, i matematici hanno detto a The Verge di aver visto un enorme aumento di tale materiale prodotto con strumenti come ChatGPT e Claude negli ultimi anni. Molto di esso è confuso, difficile da leggere e dimostra scarsa comprensione della materia; è particolarmente scadente quando si tratta di attribuire il merito ad altri ricercatori. I precedenti scritti matematici di OpenAI sono stati ampiamente criticati dagli esperti per