Jak wynika z testów przeprowadzonych przez inżyniera oprogramowania i byłego badacza kwantowego, najnowszy model OpenAI wykazał nieoczekiwaną zdolność rozwiązywania problemów matematycznych wysokiego poziomu Neela Somaniego. Somani zaobserwował, że model generuje pełne rozwiązanie po 15 minutach przetwarzania problemu w ChatGPT, a następnie sformalizował dowód za pomocą narzędzia Harmonic, potwierdzając jego dokładność. Stwierdził, że jego celem jest ustalenie punktu odniesienia dla zdolności dużych modeli językowych (LLM) do rozwiązywania otwartych problemów matematycznych. W toku myślenia modelu odwoływano się do aksjomatów matematycznych, w tym wzoru Legendre'a, postulatu Bertranda i twierdzenia o Gwieździe Dawida. Znaleziono post Math Overflow z 2013 r. autorstwa matematyka z Harvardu Noama Elkiesa, który oferował rozwiązanie podobnego problemu, ale ostateczny dowód ChatGPT różnił się i zapewniał pełniejsze rozwiązanie problemu postawionego przez matematyka Paula Erdősa. Od czasu wydania GPT 5.2, który Somani określił jako „anegdotycznie bardziej uzdolniony w rozumowaniu matematycznym niż w poprzednich iteracjach”, rosnąca liczba rozwiązanych problemów wzbudziła zapytania o zdolność LLM do pogłębiania wiedzy ludzkiej. Somani skupił się na problemach Erdősa, zbiorze ponad 1000 domysłów dostępnych w Internecie, różniących się tematyką i stopniem trudności. Pierwsze autonomiczne rozwiązania tych problemów pojawiły się w listopadzie w AlphaEvolve, modelu napędzanym silnikiem Gemini. Niedawno Somani i inni odkryli, że GPT 5.2 jest biegły w matematyce wysokiego poziomu. Od grudnia 15 problemów na stronie internetowej Erdős zmieniło się z „otwartych” na „rozwiązane”, a 11 rozwiązań opiera się na modelach sztucznej inteligencji. Matematyk Terence Tao na swoim Strona GitHubaodnotowali osiem problemów, w przypadku których modele sztucznej inteligencji poczyniły znaczące, autonomiczne postępy, oraz sześć przypadków, w których postęp polegał na lokalizowaniu wcześniejszych badań i korzystaniu z nich. Tao wysunął przypuszczenie na temat Mastodona, że skalowalny charakter systemów sztucznej inteligencji sprawia, że „lepiej nadają się one do systematycznego stosowania w przypadku„ długiego ogona ”niejasnych problemów Erdő, z których wiele ma w rzeczywistości proste rozwiązania”, dodał, że „wiele z tych łatwiejszych problemów Erdősa jest obecnie bardziej prawdopodobne, że zostanie rozwiązany metodami wyłącznie opartymi na sztucznej inteligencji niż środkami ludzkimi lub hybrydowymi”. Siłą napędową tego postępu jest zwrot w kierunku formalizacji, pracochłonnego procesu sprawdzania i rozszerzania rozumowania matematycznego. Nowe, zautomatyzowane narzędzia nie wymagają sztucznej inteligencji, ale uprościły ten proces. Asystent dowodu Lean o otwartym kodzie źródłowym, opracowany w Microsoft Research w 2013 r., zyskał szerokie zastosowanie do formalizowania dowodów, a narzędzia sztucznej inteligencji, takie jak Arystoteles firmy Harmonic, mają na celu zautomatyzowanie większości tej pracy. Tudor Achim, założyciel Harmonic, stwierdził, że zaangażowanie matematyków i profesorów informatyki w narzędzia AI ma większe znaczenie niż liczba rozwiązanych problemów Erdősa. Achim powiedział: „Ci ludzie muszą chronić reputację, więc kiedy mówią, że korzystają z Arystotelesa lub ChatGPT, jest to prawdziwy dowód”.
