W ostatni weekend Neel Somani — inżynier oprogramowania, były badacz ilościowy i założyciel startupu — natrafił na niespodziewane odkrycie podczas testów zdolności matematycznych nowego modelu OpenAI. Wkleił do ChatGPT trudne zadanie matematyczne, pozwolił modelowi pracować przez około 15 minut, a po powrocie znalazł kompletne rozwiązanie. Ocenę dowodu sformalizował przy pomocy narzędzia Harmonic — i wszystko się zgadzało.
Somani wyjaśniał, że chciał ustalić punkt odniesienia: od kiedy duże modele językowe są w stanie samodzielnie rozwiązywać otwarte problemy matematyczne, a gdzie nadal napotykają trudności. Zaskoczeniem było to, że najnowsza iteracja modelu — opisywana przez Somaniego jako GPT 5.2 — przesunęła tę granicę dalej niż wcześniejsze wersje.
W trakcie rozumowania model wygenerował imponujący „łańcuch myślowy”, przywołując znane twierdzenia i narzędzia matematyczne, m.in. wzór Legendre’a, postulat Bertranda oraz tzw. twierdzenie Gwiazdy Dawida. Model odnalazł też w sieci post z 2013 roku na MathOverflow, w którym Noam Elkies z Harvardu zaproponował eleganckie rozwiązanie podobnego problemu. Końcowy dowód przedstawiony przez ChatGPT różnił się jednak w istotny sposób od pracy Elkiesa i dostarczył pełniejszego rozwiązania wersji zadania postawionego przez Paula Erdősa — legendarnego matematyka, którego obszerna lista nierozwiązanych problemów stała się polem zmagań dla narzędzi AI.
Ten przypadek nie jest odosobniony. Narzędzia AI są coraz powszechniejsze w matematyce — od modeli nastawionych na formalizację, takich jak Aristotle od Harmonic, po narzędzia wspierające przegląd literatury, jak funkcje badawcze wprowadzane przez duże firmy. Po publikacji GPT 5.2 (przez niektórych anegdotycznie ocenianej jako lepszej w rozumowaniu matematycznym niż poprzednie wersje), rośnie liczba problemów, które modele pomagają rozwiązać, co rodzi pytania o to, na ile LLM-y mogą przesuwać granice ludzkiej wiedzy.
Somani skupiał się na tzw. problemach Erdősa — zbiorze ponad tysiąca przypuszczeń autorstwa węgierskiego matematyka, utrzymywanym publicznie online. Zakres tych problemów jest bardzo zróżnicowany zarówno pod względem tematyki, jak i trudności, dlatego stały się one atrakcyjnym celem dla matematyki wspieranej przez AI. Pierwsze samodzielne rozwiązania pojawiły się już w listopadzie w pracy opisującej model AlphaEvolve napędzany technologią Gemini (arXiv:2511.02864), ale w ostatnim czasie wielu badaczy, w tym Somani, uznało GPT 5.2 za wyjątkowo sprawny w zadaniach wysokiego poziomu.
Od Świąt Bożego Narodzenia 15 problemów z listy Erdősa zostało przesuniętych ze statusu „otwarty” do „rozwiązany” — w 11 przypadkach autorzy wyraźnie wskazali, że w procesie uczestniczyły modele AI. Z perspektywy środowiska matematycznego to istotna zmiana tempa pracy nad tą długą listą zagadnień.
Laureat Fields Medal, Terence Tao, przyjął bardziej zniuansowane stanowisko i na swojej stronie GitHub zliczył osiem różnych problemów, w których modele AI dokonały istotnego, autonomicznego postępu, oraz sześć przypadków, gdzie wkład polegał na odnalezieniu i wykorzystaniu wcześniejszych badań. To pokazuje, że chociaż nadal daleko do scenariusza, w którym systemy AI robią matematykę całkowicie bez udziału człowieka, to jednak modele mogą pełnić ważną, uzupełniającą rolę.
Jednym z czynników przyspieszających ten proces jest rosnące zainteresowanie formalizacją dowodów — pracochłonnym zadaniem, które ułatwia weryfikację i dalsze rozwijanie rozumowań. Formalizacja nie wymaga stosowania AI, lecz pojawienie się narzędzi automatyzujących ten proces znacząco obniża próg wejścia. Otwarty system „proof assistant” Lean, rozwijany od 2013 roku, zyskał szerokie zastosowanie jako narzędzie do formalizowania dowodów, a systemy takie jak Aristotle od Harmonic obiecują automatyzację dużej części pracy związanej z formalizacją.
Dla Tudora Achima, założyciela Harmonic, ważniejsze od liczby rozwiązanych problemów Erdősa jest fakt, że czołowi matematycy i informatycy zaczynają poważnie korzystać z tych narzędzi. „Bardziej zależy mi na tym, że profesorowie matematyki i informatyki wykorzystują [narzędzia AI]” — mówi Achim. — „Ludzie ci dbają o swoją reputację, więc kiedy mówią, że używają Aristotle’a lub ChatGPT, to jest realny dowód.”