I vad som bara kan beskrivas som den akademiska motsvarigheten till att tappa ett piano i huvudet på någon och sedan be dem recensera noterna, släppte OpenAI denna vecka nästan 400 AI-genererade matematiska resultat utspridda över mer än 700 manuskript. Reaktionerna från matematikvärlden sträckte sig från "häpnadsväckande" till "ren galenskap" – och det var de artiga.

Samlingen spänner över kombinatorik, flera grenar av geometri, talteori, teoretisk datavetenskap, algebra, topologi, sannolikhetsteori och statistisk mekanik samt matematisk fysik. Den är så omfattande att OpenAI kände sig tvungna att publicera vägledning för hur man navigerar i det vidsträckta GitHub-förrådet, vilket är lite som att ge någon en karta till en byggnad du just satt eld på.

"Bara att gå igenom hela listan med sammanfattningar är överväldigande", säger Álvaro Lozano-Robledo, professor i matematik vid University of Connecticut. Flera matematiker berättade för The Verge att bara arbetet med att ta sig igenom den cirka 40 sidor långa innehållsförteckningen och sammanfattningarna tog dem en dryg timme. För den som håller räkningen där hemma: en timme bara för att läsa menyn.

Bland de hundratals manuskripten finns formaliseringar i Lean, ett programmeringsspråk och bevisassistent som gör att resultat kan verifieras beräkningsmässigt. Dessa formaliseringar har visat sig avgörande för att bedöma några av OpenAIs tidigare matematiska påståenden, vilket ger forskare förtroende för att ett påstående är logiskt korrekt även om de inte helt förstår argumentet bakom – vilket är lite som att lita på en miniräknare utan att veta vad division är.

Men graden av verifiering varierade kraftigt. På GitHub medgav OpenAI att resultaten befinner sig "i olika stadier av verifiering" och att "många, men inte alla, av manuskripten har formaliserats". Vid skrivandet verkar färre än hälften av manuskripten i samlingen ha beskrivits formellt. OpenAI uppgav att endast 300 toppresultat av 719 manuskript hade formaliserats – cirka 42 procent – och att man "kommer att uppdatera förrådet med fler formaliseringar när vi får dem". Så ungefär 58 procent av den matematiska apokalypsen förblir overifierad. Sov gott.

Flera matematiker klagade till The Verge över bristen på formalisering, särskilt med tanke på det enorma antalet resultat. Även när Lean-kod åtföljer ett resultat är utvärderingen inte omedelbar. Forskare måste kontrollera att formaliseringen faktiskt bevisar det resultatet påstår – ännu en tidskrävande process. Flera som grävt i artiklarna sade att även där datorverifierbara bevis tillhandahållits var kvaliteten inkonsekvent och de påståenden de verifierade inte alltid tycktes motsvara påståendena i medföljande manuskript.

Kevin Buzzard, professor i matematik vid Imperial College London, sade att han hade identifierat många teorem inom sitt arbetsområde – algebraisk talteori – av vilka endast omkring sex omedelbart "stack ut". Få, om ens några, av dessa tycktes vara formellt verifierade i Lean. "Därför måste jag antingen läsa möjligen inte korrekt slop, eller vänta på att andra gör samma sak, eller vänta på att någon formaliserar dem innan jag säkert kan säga att resultaten ens är korrekta." Buzzards farhågor ekades av många andra forskare, som förmodligen hade annat att göra denna vecka.

Buzzard var långt ifrån ensam om att oroa sig för AI-"slop" – en förkortning för lågkvalitativt, ofta felaktigt AI-genererat material som alltmer dyker upp online och i verkligheten, inklusive i akademiska artiklar. Liksom inom andra områden berättade matematiker för The Verge att de sett en enorm ökning av sådant material producerat med verktyg som ChatGPT och Claude under de senaste åren. Mycket av det är förvirrande, svårläst och visar liten förståelse för ämnet; det är särskilt uselt när det gäller att kreditera andra forskare. OpenAIs tidigare matematiska skrifter kritiserades brett av experter för