OpenAI wycofało trzy manuskrypty matematyczne po tym, jak błąd znaku unieważnił kluczowy argument oraz konstrukcję wykorzystaną w dwóch zależnych od niej pracach. Historię repozytorium z tym wpisem opublikowano 7 października 2026 roku, dzień po udostępnieniu przez OpenAI zbioru wyników. Wpis odnotował również poprawki w innych manuskryptach i dodatkowe formalizacje w Lean.
Trzy manuskrypty wycofane po błędzie znaku
Według historii repozytorium błąd znaku unieważnił argument dotyczący skracania śladu stabilizacyjnego oraz konstrukcję wykorzystaną w dwóch zależnych pracach. OpenAI wycofało trzy manuskrypty. To konkretna korekta dotycząca tych prac, nie werdykt o całym zbiorze wyników.
Wpis z 7 października wymienia tytuły wycofanych prac: „Algebraicity of Weil classes on split abelian eightfolds”, „Algebraicity of Kuga–Satake Correspondences for K3 Surfaces” oraz „The rational Hodge conjecture for products of K3 surfaces”.
Krytyka publikacji ze strony AHM
Po udostępnieniu zbioru 6 października Association for Human Mathematics (AHM) sprzeciwiło się skali publikacji. Organizacja podała, że jednorazowo udostępniono ponad 700 plików, i oceniła, że taka forma prezentacji demonstruje siłę, a nie dorobek naukowy. Wezwała też matematyków do zakończenia współpracy z OpenAI.
Wcześniejszy spór dotyczący twierdzenia OpenAI o równaniach Naviera–Stokesa opisaliśmy w osobnym materiale. Obecna aktualizacja dotyczy odrębnego zbioru prac matematycznych i jego poprawek.
Jak OpenAI opisało publikację wyników
OpenAI opublikowało wyniki wygenerowane przez wewnętrzny model w repozytorium GitHub. Firma opisała protokoły przeglądu prac i cytowania, a także udostępnione informacje o zadaniach podejmowanych przez model, szacunkach obliczeń i podsumowaniach jego rozumowania. Podała, że opublikowała 10 takich podsumowań.
OpenAI informowało również o konsultacjach z niezależną grupą Institute for Advanced Study Advisory Group on Mathematics and Artificial Intelligence i o uwzględnianiu jej publicznych rekomendacji w praktykach publikacyjnych. Firma podawała średnio około trzech godzin obliczeń rozumowania w przeliczeniu na ChatGPT Pro na jeden wynik.
Co oznacza liczba formalizacji w Lean
Lean to język i asystent dowodzenia, który pozwala zapisać twierdzenie oraz dowód w postaci sprawdzalnej przez komputer. Wpis w historii repozytorium z 7 października podaje, że formalizację w Lean miało 300 z 719 głównych wyników — około 42%.
Ta liczba opisuje formalizację, a nie liczbę wyników niezależnie zaakceptowanych przez matematyków. Asystent dowodzenia sprawdza zapisany dowód względem przyjętych definicji i założeń; samo sprawdzenie nie rozstrzyga, czy formalny zapis odpowiada zamierzonemu twierdzeniu ani czy wynik jest użyteczny dla dalszych badań.
Pozostałe zmiany w repozytorium
Historia repozytorium OpenAI z 7 października odnotowuje także korekty 14 manuskryptów, aktualizacje cytowań w kolejnych 13 pracach oraz sześć dodatkowych formalizacji. To osobne pozycje wpisu, obok trzech wycofanych manuskryptów.
