OpenAI: dziesięć wyników matematycznych sformalizowanych w Lean i rola wewnętrznego modelu

1 sierpnia OpenAI opublikowało manuskrypt „Ten Advances in Mathematics and Theoretical Computer Science”, przypisując wyniki własnemu wewnętrznemu modelowi. Równocześnie powstało repozytorium GitHub `openai/ten-proofs`, które udostępnia formalizacje wszystkich dziesięciu dowodów w Lean 4. Wśród wyników wyróżniają się: poprawa wykładnika dla upakowania sfer — pierwsza od 1978 roku —, konstrukcja grupy niesoficznej oraz kontrprzykład dla hipotezy sztywności Connesa. Repozytorium to projekt Lean 4.32.0 oparty na mathlib, wydany na licencji Apache-2.0: każdy może ponownie skompilować dowody poleceniami `lake exe cache get` i `lake build All`, a katalog ComparatorChallenges wyjaśnia, jak przeprowadzić weryfikację niezależnie.

Media powiązały te wyniki z „Astrą”, nazwą kolejnej rodziny modeli ogłoszonej przez OpenAI tego samego 1 sierpnia; manuskrypt mówi jednak wyłącznie o „wewnętrznym modelu”, który nie został udostępniony. Dane takie jak koszt około 2000 dolarów w tokenach czy 249 stron dokumentu pochodzą z relacji podmiotów trzecich, ponieważ oficjalna strona ogłoszenia jest obecnie niedostępna. Praca zawiera podziękowania dla ludzkich matematyków za korektę i wskazuje na niezależną, równoległą pracę Shuoxinga Zhou, powstałą częściowo z pomocą GPT-5.6 Sol.

Według SiliconANGLE argumenty matematyczne pochodzą od modelu, ale to ludzcy badacze przekształcili jego wynik w manuskrypty nadające się do publikacji: nie wiadomo, jak wiele waży ta obróbka. Użycie Lean 4 przesuwa punkt ciężkości dyskusji: certyfikat gwarantuje logiczną poprawność dowodu, lecz nie potwierdza automatycznie, że sformalizowane twierdzenie pokrywa się z historycznym otwartym problemem — ta kontrola pozostaje w rękach ludzi. Żaden z dziesięciu wyników nie przeszedł formalnej recenzji naukowej. Precedens ciąży: w październiku 2025 roku ogłoszenie, że GPT-5 „rozwiązał” dziesięć problemów Erdősa, okazało się bezpodstawne, a Thomas Bloom, opiekun erdosproblems.com, nazwał je poważnym przeinaczeniem. O dzisiejszych dziesięciu wynikach ten sam Bloom mówi natomiast „big news”. Jak zauważa fizyk teoretyczny Tobias J. Osborne, przytaczane 2000 dolarów to koszt zwycięskich tokenów, a nie całkowity plon wszystkich prób — o tym OpenAI nie podało żadnych informacji. Wszystko to wpisuje się w kontekst „Leiden Declaration on Artificial Intelligence and Mathematics”, ogłoszonej w czerwcu 2026 roku i popartej, według the-decoder, przez ponad 3000 matematyków oraz przez International Mathematical Union; deklaracja domaga się przejrzystości, ochrony praw autorów i ludzkiej odpowiedzialności za wyniki.

Prawdziwą nowiną nie jest to, że maszyna uprawiała matematykę — dzieje się to od miesięcy — lecz to, że tym razem każdy wynik przychodzi z certyfikatem Lean, który można ponownie skompilować: żeby ocenić, nie trzeba wierzyć ogłaszającemu. Dopóki jednak stosunek nieudanych prób do sukcesów pozostanie tajemnicą przedsiębiorstwa, ocena efektywności tych modeli będzie raczej ćwiczeniem z wiary niż ze statystyki.