Afiliacja: ulam.ai
Thomas Bloom to brytyjski matematyk, który od kilku lat prowadzi stronę erdosproblems.com. Paul Erdős zostawił po sobie ponad tysiąc problemów – głównie z teorii liczb i kombinatoryki – z których wiele do dzisiaj pozostaje nierozwiązanych. Bloom stara się zebrać je wszystkie i skatalogować.
Pod koniec grudnia 2025 roku na stronie Blooma zaczął panować ruch większy niż zwykle. Nowe wpisy, nowe podejścia do starych problemów, pierwsze udane ataki na problemy, którymi nikt nie zajmował się od 50 lat. Powód? Pojawienie się GPT-5.2 od OpenAI w publicznym dostępie.
Terence Tao jest jednym z najbardziej znanych matematyków na świecie. Medalista Fieldsa, niestrudzony edukator, który prowadzi poczytny blog, ma na swoim koncie liczne wykłady na świecie i skupia wokół siebie dziesiątki współpracowników. Ostatnio znalazł sobie nowe hobby – AI. Dawniej sceptyk – zachowały się jego wypowiedzi, w których wątpi w szeroką użyteczność sztucznej inteligencji – obecnie realista-eksperymentator. Dopiero co nagrał na YouTube film (youtu.be/JHEO7cplfk8?si=TRjhuae2bfEyg4ce) o tym, jak używa Claude Code do formalizacji swojego dowodu w Lean.
Lean to język programowania i asystent dowodzenia, w którym można zapisywać twierdzenia matematyczne i ich dowody w sposób zrozumiały dla komputera. Program weryfikuje każdy krok rozumowania, dzięki czemu raz sformalizowany dowód jest pewny – nie ma w nim luk ani błędów, które mogą umknąć ludzkiemu recenzentowi.
Tao jest też jednym z najbardziej aktywnych użytkowników forum Blooma. Jego wpisy pojawiają się prawie codziennie, często odpowiada, komentuje, uzupełnia kontekst, identyfikuje trudności w problemach. To dzięki niemu kilka problemów Erdősa zostało rozwiązanych za pomocą AI.
Co się zmieniło z nadejściem GPT-5.2?
Rozumowanie. Przeskok pomiędzy tym a poprzednimi modelami z mojej perspektywy jest większy niż jakakolwiek zmiana, która dokonała się wcześniej. Wydłużył się kontekst i okienko rozumowania. Oznacza to, że model może przyjąć więcej danych i dłużej się nad nimi zastanawiać – rozumowania w wersji Pro Extended Thinking potrafią trwać nawet 80–90 minut na jedno zapytanie.
Dzięki temu postępowi komentarz Tao, który zarysowuje strategię ataku na problem, można użyć jako prompt do GPT-5.2 (a obecnie 5.4), który prowadzi bezpośrednio do gotowej pracy. Takich przykładów, prompt \(\leadsto\) gotowa praca matematyczna, było już kilka.
LLM (ang. large language model) – model uczenia maszynowego trenowany na bardzo dużych zbiorach tekstów, który uczy się przewidywać kolejne słowa w zdaniu, typowo z wykorzystaniem architektury transformera. W praktyce pozwala to na generowanie spójnych odpowiedzi, często brzmiących jak napisane przez człowieka, a także na analizę i przetwarzanie tekstu oraz pracę z kodem. Przykładem LLM jest rodzina modeli GPT omawiana w tekście.
LLM-y są w stanie też radzić sobie bez komentarzy medalistów Fieldsa. Sam jestem częstym bywalcem forum i dzięki GPT-5.2 oraz GPT-5.4, a także procesowi, który trwał dwa miesiące, rozwiązałem problem Erdősa nr 1148. Problem ten ma elementarne sformułowanie: czy każda duża liczba całkowita \(n\) daje się przedstawić (dla pewnych całkowitych \(x,y,z\)) w postaci \(n = x^2 + y^2 - z^2\) z warunkiem \(\textrm{max}(x^2,y^2,z^2) \leq n\)?
Rozwiązanie jednak elementarne nie jest i wykorzystuje twierdzenie Duke’a o dystrybucji punktów na hiperboloidach. W znalezieniu go pomogła mi wiedza z teorii liczb, dzięki czemu proces przypominał prowadzenie doktoranta do rozwiązania. Mimo to GPT-5.2 nie był w stanie ukończyć problemu, za to GPT-5.4 niemal od razu zobaczył poprawne rozwiązanie na bazie poprzednich notatek.
Pełne rozwiązanie można zobaczyć pod adresem www.ulam.ai/research/erdos1148-full.pdf, a dyskusję tu: www.erdosproblems.com/1148.
O rozstrzygnięciu przez sztuczną inteligencję bardzo znanej hipotezy Erősa, które zostało ogłoszone już po wstępnym złożeniu niniejszego wydania Delty, piszemy tutaj
AI jako matematyk
AI oczywiście jeszcze nie jest w pełni autonomicznym matematykiem – ale jest to kierunek, którym się zajmuję w ramach mojej działalności zawodowej, jak również zajmuje się tym kilka firm na świecie: Axiom, Math Inc., Harmonic. LLM-y są znakomite w wyszukiwaniu literatury przedmiotu i stosowaniu rozumowań, które są już dostępne w innych kontekstach, ale w tej samej działce. Za to absolutnie nie są jeszcze zdolne do budowania nowych definicji i teorii ani do brania inspiracji z innych dziedzin (chyba że zostały do tego popchnięte promptami explicite).
Niemniej to, do czego już są zdolne, sprawia, że praca matematyka (a także naukowca z dowolnej dziedziny) znacząco przyspiesza. AI jest w stanie bardzo dokładnie przeszukać literaturę, zaprojektować eksperymenty na wybranych przykładach, zaproponować strategie dowodowe i niektóre samemu przeprowadzić.
Dlatego zachęcam każdego matematyka i pasjonata do spróbowania GPT-5.4 Extended Thinking (koniecznie Extended Thinking): wystarczy zacząć od załadowania modelowi swojej ostatniej pracy i poproszenia o możliwe kontynuacje i rozwinięcie tematu, by zobaczyć, do czego jest zdolny.
Praca matematyka w najbliższych latach mocno się zmieni. Odpowiedź na pytanie jak to już temat na osobny artykuł. Innym ważnym wątkiem jest też formalizacja matematyki w Lean. Dziedzina, która jeszcze niedawno była niewielką niszą, jest obecnie jedną z najszybciej rozwijających się gałęzi matematyki. W końcu chcemy mieć możliwość weryfikacji, że dowody, które produkują agenci AI, są poprawne.
Tutaj największy przełom dokonał się niedawno, w 2026 roku. Firma Math Inc zbudowała bowiem Gaussa – agenta AI, który, działając nieprzerwanie przez 2 tygodnie (bazując na dodatkowej współpracy z ludźmi), sformalizował dowody Maryny Wiazowskiej problemu upakowania sfer, za które otrzymała medal Fieldsa. Formalizacja zajęła 200 000 linii kodu w Lean.
Wkraczamy na nowe, nieznane terytorium w prowadzeniu badań, w tym matematycznych. AI obiecuje demokratyzację „inteligencji”, a co za tym idzie, przyspieszenie generowania pomysłów, dowodów, twierdzeń. Jest jeszcze wiele do zrobienia, ale rzeczywistość matematyka zmieniła się w grudniu 2025 roku. Jestem optymistą i wierzę, że zmiana ta jest tylko na lepsze.