OpenAI publikuje 722 prace matematyczne. Chaos czy przełom?

Na początku tygodnia OpenAI udostępniło pokaźny zbiór wyników matematycznych, który według firmy ma „przesuwać granice ludzkiej wiedzy”. Mowa o 722 pracach dotyczących 372 otwartych problemów – od algebry i geometrii po informatykę teoretyczną. Większość z nich powstała przy udziale niewydanego jeszcze modelu sztucznej inteligencji. Skala i forma tej publikacji wywołały w środowisku matematycznym prawdziwe trzęsienie ziemi.

Kilka tekstów zostało już wycofanych lub poprawionych, a sam sposób ujawnienia wyników określano mianem „zrzutu”, „wysypiska”, a nawet „matematycznej apokalipsy”. Część prac dotyczy problemów najwyższej rangi, w tym hipotezy Riemanna oraz hipotezy Bircha i Swinnertona-Dyera – każde rozwiązanie któregoś z nich wiąże się z nagrodą miliona dolarów w ramach Problemów Milenijnych.

Dlaczego OpenAI to zrobiło i czy wynikom można wierzyć?

Odpowiedzi na te dwa pytania nie są oczywiste. Firma przekonuje, że celem publikacji jest „umożliwienie dalszego postępu w matematyce”. Sposób udostępnienia materiału niekoniecznie jednak temu sprzyja. Jeden z seniorów w środowisku akademickim, cytowany przez autorkę analizy, znalazł w zbiorze jedno ze swoich ulubionych zagadnień i próbował przeczytać towarzyszącą mu pracę. Jak relacjonował, tekst okazał się tak niezrozumiały, że gdyby trafił do niego jako redaktora czasopisma matematycznego, „wylądowałby prosto w koszu”.

Co ciekawe, nawet własny model OpenAI – ChatGPT w wersji GPT-5.6 Sol – okazał sceptycyzm, gdy zapytano go o jeden z głośniejszych wyników. Opisał go jako „poważną halucynację”, która „nie powinna być cytowana, zgłaszana ani rozpowszechniana jako dowód bez pełnego audytu eksperckiego”. Innymi słowy, mimo potencjalnie przełomowego charakteru części rezultatów, forma ich przedstawienia bywa nieczytelna nawet dla specjalistów.

Zmiana narracji i cień poprzedniej kontrowersji

Jednym z możliwych motywów stojących za publikacją jest chęć odwrócenia uwagi od wcześniejszej głośnej sprawy. We wrześniu OpenAI ogłosiło kontrowersyjne rozwiązanie szczególnego przypadku problemu Naviera-Stokesa, kolejnego zagadnienia z listy milenijnych. Matematycy Tristan Buckmaster i Levent Alpöge, którzy sami pracowali nad tym problemem, oskarżyli firmę o wykorzystanie ich danych i pomysłów, a następnie przeznaczenie około 15 milionów dolarów mocy obliczeniowej na znalezienie rozwiązania. OpenAI zaprzeczyło tym zarzutom.

Drugi potencjalny powód ma szerszy wymiar – chodzi o sztuczną inteligencję ogólną (AGI), czyli hipotetyczny system przewyższający ludzi w zasadzie we wszystkich zadaniach poznawczych. Matematyka, zwłaszcza czysta i abstrakcyjna, uchodzi za dziedzinę wymagającą bardzo złożonego rozumowania dowodowego i trudną dla większości ludzi. Zdolność modeli OpenAI do prowadzenia badań na poziomie naukowym może więc wzmacniać narrację, że systemy te zbliżają się do celu, jakim jest AGI. Taka narracja może przynieść firmie korzyści przed planowanym debiutem giełdowym – według doniesień OpenAI liczy na wycenę sięgającą 1,4 biliona dolarów, czyli około 4% PKB Stanów Zjednoczonych.

Jak zweryfikować poprawność matematyki?

Matematyka, szczególnie czysta, opiera się na obiektywnej prawdzie – twierdzenia są albo prawdziwe, albo fałszywe, a niejednoznaczność niemal nie występuje. Od stuleci o prawdziwości ustaleń decyduje konsensus środowiska. Nowe prace przechodzą recenzję ekspertów, którzy sprawdzają poprawność przed publikacją i włączeniem do obiegu naukowego. Proces bywa czasochłonny – niektóre obszerne i techniczne teksty recenzuje się latami.

Ostatecznym testem dla wyników OpenAI będzie więc to, co zrobi z nimi społeczność matematyczna po rzetelnym zbadaniu. Firma wycofała już trzy prace z powodu elementarnego błędu i poprawiła kilka innych, w których pomyłki unieważniały rezultaty. Wskazuje to przynajmniej na niewystarczającą weryfikację przed publikacją.

Maszyny sprawdzające maszyny

Od ponad dekady trwa ruch na rzecz „formalizacji” wyników przy użyciu systemów takich jak Lean. Narzędzia te budują matematykę od podstawowych zasad i aksjomatów, dzięki czemu mogą sprawdzić każdy krok logiczny dowodu. Do niedawna formalizacja dotyczyła głównie teorii i problemów już rozwiązanych – jednym z wczesnych przykładów była formalizacja twierdzenia o czterech barwach z teorii grafów z 2008 roku.

Formalizowanie wyniku wymaga dużej wiedzy i nakładu pracy. Obecnie systemy AI wykorzystuje się jednak do „autoformalizacji”, czyli automatycznego przekładania rezultatu na dowód możliwy do sprawdzenia maszynowo. Aby wzmocnić zaufanie do poprawności swoich wyników, OpenAI twierdzi, że sformalizowało 300 głównych rezultatów w momencie publikacji. Nie wszystkie formalizacje są jednak wykonane prawidłowo – istnieją wcześniejsze dowody na problemy z formalizacjami generowanymi przez AI, w tym w przypadku problemu Naviera-Stokesa. Nie jest obecnie jasne, czy środowisko matematyczne zaakceptuje formalizacje OpenAI.

Ekscytacja wymieszana z niepokojem

Reakcje na publikację są mieszane – od opinii, że to „oczywiście najważniejszy moment w historii matematyki”, po stwierdzenia, że matematycy „nie są zachwyceni wielką kupą na ich progu”. Ekscytacja postępem w ważnych problemach jest realna, zwłaszcza gdy eksperci zaczynają przeglądać wyniki z najdrobniejszymi szczegółami. Towarzyszy jej jednak niepewność i troska.

Pojawiają się pytania o to, co wolumen i tempo tych odkryć oznaczają dla przyszłości badań matematycznych oraz dla wkładu poszczególnych naukowców. Kto powinien dźwigać ciężar rozszyfrowywania wywodów, które na pierwszy rzut oka wyglądają jak „AI slop”? Publikacja zmusza środowisko do refleksji nad tym, co jest w matematyce naprawdę cenione – szczególnie istotnej dla studentów i badaczy na wczesnym etapie kariery, którzy muszą mierzyć się z wizją wyprzedzenia ich pracy przez ambitnego użytkownika AI oraz z pytaniem, jak ich własny dorobek będzie wyceniany.

Ta debata nie zakończy się szybko. Nawet gdy opadnie kurz po najnowszej publikacji, pytania o zaufanie, weryfikację i rolę człowieka w matematyce pozostaną otwarte. Być może najważniejszym rezultatem całego zajścia nie będą same dowody, lecz wymuszona dyskusja o granicach między automatyzacją a naukową rzetelnością.