W czymś, co można opisać jedynie jako akademicki odpowiednik zrzucenia komuś fortepianu na głowę, a następnie poproszenia go o recenzję nut, OpenAI w tym tygodniu wypuściło prawie 400 wygenerowanych przez AI wyników matematycznych rozłożonych na ponad 700 manuskryptów. Reakcja środowiska matematycznego wahała się od „oszałamiające” do „czyste szaleństwo” – i to były te uprzejme.

Kolekcja obejmuje kombinatorykę, kilka gałęzi geometrii, teorię liczb, teoretyczną informatykę, algebrę, topologię, prawdopodobieństwo i mechanikę statystyczną oraz fizykę matematyczną. Jest tak ogromna, że OpenAI poczuło się w obowiązku opublikować wskazówki, jak poruszać się po rozległym repozytorium GitHub, co jest trochę jak wręczenie komuś mapy budynku, który właśnie podpaliłeś.

„Samo przejrzenie całej listy streszczeń jest przytłaczające” – powiedział Álvaro Lozano-Robledo, profesor matematyki na Uniwersytecie Connecticut. Kilku matematyków powiedziało The Verge, że samo przejście przez około 40-stronicowy spis treści i streszczenia zajęło im dobrą godzinę. Dla tych, którzy liczą w domu: to godzina na przeczytanie samego menu.

Wśród setek manuskryptów rozsiane są formalizacje w Lean, języku programowania i asystencie dowodowym, który pozwala na komputerową weryfikację wyników. Te formalizacje okazały się kluczowe w ocenie niektórych wcześniejszych twierdzeń matematycznych OpenAI, dając badaczom pewność, że twierdzenie jest logicznie poprawne, nawet jeśli nie do końca rozumieją argumentację za nim – co jest trochę jak zaufanie kalkulatorowi bez wiedzy, czym jest dzielenie.

Ale stopień weryfikacji każdego wyniku był skrajnie różny. Na GitHubie OpenAI przyznało, że wyniki są „na różnych etapach weryfikacji” i że „wiele, ale nie wszystkie, manuskryptów zostało sformalizowanych”. W momencie pisania tego tekstu mniej niż połowa manuskryptów w kolekcji wydaje się być opisana formalnie. OpenAI powiedziało, że tylko 300 głównych wyników z 719 manuskryptów zostało sformalizowanych – około 42 procent – i że „będzie aktualizować repozytorium o kolejne formalizacje, gdy je uzyska”. Czyli około 58 procent matematycznej apokalipsy pozostaje niezweryfikowane. Śpijcie spokojnie.

Kilku matematyków poskarżyło się The Verge na brak formalizacji, zwłaszcza biorąc pod uwagę ogromną liczbę wyników. Nawet gdy kod Lean towarzyszy wynikowi, ocena nie jest natychmiastowa. Badacze muszą sprawdzić, czy formalizacja faktycznie dowodzi tego, co twierdzi wynik – kolejny czasochłonny proces. Kilku przeglądających prace stwierdziło, że nawet tam, gdzie dostarczono komputerowo weryfikowalne dowody, jakość była niespójna, a zweryfikowane twierdzenia nie zawsze wydawały się dokładnie odpowiadać twierdzeniom z towarzyszących manuskryptów.

Kevin Buzzard, profesor matematyki w Imperial College London, powiedział, że zidentyfikował liczne twierdzenia w swojej dziedzinie – algebraicznej teorii liczb – z których tylko około sześciu natychmiast „się wyróżniło”. Niewiele, jeśli w ogóle, z nich wydawało się być formalnie zweryfikowanych w Lean. „W związku z tym albo muszę czytać prawdopodobnie niepoprawny szlam, albo czekać, aż inni zrobią to samo, albo czekać, aż ktoś je sformalizuje, zanim będę mógł powiedzieć na pewno, że wyniki są w ogóle poprawne”. Obawy Buzzarda podzielało wielu innych badaczy, którzy przypuszczalnie mieli w tym tygodniu inne rzeczy do roboty.

Buzzard nie był osamotniony w martwieniu się o AI „szlam” – skrót oznaczający niskiej jakości, często błędny materiał generowany przez AI, który coraz częściej pojawia się online i w realnym świecie, w tym w pracach naukowych. Podobnie jak w innych dziedzinach, matematycy powiedzieli The Verge, że w ostatnich latach zaobserwowali ogromny wzrost takich materiałów tworzonych za pomocą narzędzi takich jak ChatGPT i Claude. Wiele z nich jest mylących, trudnych do czytania i wykazuje niewielkie zrozumienie tematu; jest szczególnie kiepskie, jeśli chodzi o przypisywanie zasług innym badaczom. Wcześniejsze prace matematyczne OpenAI były szeroko krytykowane przez ekspertów za