Przez lata sztuczna inteligencja w matematyce kojarzyła się głównie z edukacją (rozwiązywanie zadań krok po kroku) albo z „ładnymi sztuczkami” w symbolice. W 2025 i na początku 2026 r. narracja zaczęła się jednak przesuwać: AI coraz częściej działa jak asystent badawczy (szuka tropów w literaturze), generator hipotez (proponuje konstrukcje), a w najlepszych przypadkach – jako narzędzie, które potrafi doprowadzić do formalnie weryfikowalnego dowodu.
TechCrunch opisał falę przypadków, w których najnowsze modele – w tym ChatGPT – były wykorzystywane do rozwiązywania trudnych problemów z listy Paula Erdősa, a część rozwiązań została później sprawdzona i sformalizowana w narzędziach do weryfikacji dowodów. Jednocześnie samo środowisko matematyczne podkreśla, że kluczowe jest odróżnienie dwóch zjawisk:
- AI odnajduje istniejące już rozwiązania w literaturze
- AI faktycznie generuje nowe kroki rozumowania – i dopiero formalizacja pozwala to w miarę bezpiecznie rozstrzygać.
Spójrzmy na to, co dokładnie AI już „umie” w matematyce, na jakich przykładach to widać – i dlaczego najbardziej zmienia się dziś nie „wynik”, lecz proces.
Najważniejsza zmiana: matematyka zaczyna się formalizować (a AI pomaga w tym najbardziej)
W nowoczesnej matematyce problemem bywa nie to, że dowodu „nie ma”, tylko że:
- jest rozproszony po publikacjach,
- jest trudny do zweryfikowania i ponownego użycia.
Dlatego rośnie znaczenie tzw. proof assistants – narzędzi takich jak Lean, które pozwalają zamienić dowód na formalny zapis możliwy do automatycznego sprawdzenia. TechCrunch w przywołanym już tekśćie zwraca uwagę, że AI coraz częściej pełni rolę „silnika formalizacji”, przyspieszając żmudne przełożenie ludzkiego rozumowania na kod dowodu. To nie jest detal techniczny – to zmiana paradygmatu: zaufanie przesuwa się z „autorytetu autora” na „weryfikowalność w narzędziu”.
Wyzwania Erdősa: AI domyka problemy z długiej listy
Paul Erdős wielkim matematykiem był. To jasne jak to, że dwa razy dwa jest cztery. Fascynowały go koncepcje matematyczne dotyczące teorii liczb, kombinatoryki i teorii grafów. A jako że w swych matematycznych podróżach nie raz i nie dwa natrafiał na równania zbyt trudne do rozwiązania, to zaczął wyznaczać nagrody pieniężne dla tych, którzy potrafiliby się z nimi uporać.
Nie zdziwicie się chyba, jeśli napiszemy, że takich zdolnych śmiałków było niewielu. Erdősowe wyzwania pozostały aktualne do dziś.
TechCrunch przywołał przypadek, w którym użytkownik testował nowe modele na problemach z serwisu erdosproblems.com (baza ponad tysiąca problemów i hipotez Erdősa), a następnie oceniał rozwiązanie i formalizował je w narzędziu do weryfikacji (w tekście pojawia się Harmonic i ich system). W artykule pojawia się też ważny kontekst: część „postępu” AI wynika z tego, że model potrafi odnaleźć i wykorzystać istniejące rozwiązania. Udało się na przykład dotrzeć przez model do wątku na MathOverflow, gdzie Noam Elkies podawał elegancką metodę dla pokrewnego problemu.
Równolegle w społeczności erdosproblems.com toczy się dyskusja o tym, jak poprawnie cytować literaturę, gdy AI „opiera się” na wcześniejszych wynikach, ale nie ujawnia tego wprost w finalnym wywodzie. Czy można więc cieszyć się, że AI już dziś bywa skuteczna w „długim ogonie” problemów, zwłaszcza tam, gdzie rozwiązanie jest krótkie, ale ukryte w literaturze lub wymaga cierpliwego „dopięcia” szczegółów?
AI na poziomie olimpijskim: to nie „otwarte tezy”, ale twardy test rozumowania i dowodzenia
Jednym z najbardziej widocznych postępów jest przejście od „wyniku” do dowodu krok po kroku. DeepMind pokazało w 2024 roku, że ich systemy (AlphaGeometry i późniejsze wersje) potrafią rozwiązywać zadania geometryczne w stylu Międzynarodowej Olimpiady Matematycznej (IMO) na bardzo wysokim poziomie.
W 2025 r. Nature opisywało, że modele DeepMind i OpenAI osiągały rezultaty porównywalne z topowymi uczestnikami IMO. To nadal nie jest „rozwiązanie problemu milenijnego”, ale jest to znaczące, bo IMO wymaga kreatywności i rygoru dowodowego.
FunSearch i nowe konstrukcje dla problemu cap set
Jednym z najczęściej cytowanych przypadków AI, która faktycznie „pchnęła” matematykę do przodu, jest FunSearch. DeepMind opisało, że system znalazł nowe konstrukcje dla problemu cap set (z ekstremalnej kombinatoryki), poprawiając wcześniejsze najlepsze wyniki dla wybranych rozmiarów. Co ważne: to nie jest sytuacja „AI przeczytała Internet i streściła”. Tu mechanizm polega na tym, że model generuje programy-kandydaty, a system ewolucyjnie wybiera te, które dają lepszy wynik – czyli AI jest zaprzęgnięta do przeszukiwania gigantycznej przestrzeni rozwiązań.
Nowe algorytmy mnożenia macierzy (AlphaTensor)
Matematyka nie kończy się na twierdzeniach – często chodzi o algorytmy. W 2022 r. Nature opublikowało pracę o AlphaTensor, systemie DeepMind, który odkrywa wydajniejsze algorytmy mnożenia macierzy (fundamentalna operacja w nauce, grafice, ML).
To przykład, gdzie AI nie „udowadnia twierdzenia”, ale znajduje lepszą konstrukcję obliczeniową – i to również jest wkład do matematyki i informatyki teoretycznej.
Nowa fala 2025/2026: narzędzia hybrydowe (LLM + ewolucja + weryfikacja)
Ciekawym kierunkiem jest łączenie LLM z automatyczną oceną i selekcją rozwiązań – tak działa m.in. AlphaEvolve, opisywany zarówno w pracy na arXiv, jak i w komunikacji DeepMind: model proponuje modyfikacje kodu/rozwiązania, a system je testuje i iteracyjnie ulepsza. Równolegle firmy skupione na formalnym dowodzeniu (np. Harmonic) promują podejście, w którym wynik ma być nie tylko „przekonujący”, ale od razu sprawdzalny formalnie (Lean).
Jeśli już zakręciło się Wam w głowie od tych wszystkich złożonych matematycznych terminów, przejdźmy do logiki. Czyli spróbujemy logicznie wywnioskować, czy rozwój AI przyczyni się do rozwiązania piętrzących się w podręcznikach problemów.
Szybsze domykanie „mniejszych wielkich problemów – czy rzeczywiście? Nie każdy problem jest hipotezą Riemanna (uff!) Matematykę tworzą tysiące mniejszych pytań, lematów i konstrukcji. AI – jak zauważa TechCrunch, przywołując wypowiedzi Terence’a Tao – może być szczególnie dobra w „systematycznym” atakowaniu takiego długiego ogona.
Wzrośnie znaczenie formalizacji i narzędzi weryfikacji? Jeśli AI ma współtworzyć matematykę, społeczność będzie coraz mocniej wymagała, by wynik dało się zweryfikować maszynowo. Lean i podobne narzędzia stają się „wspólnym językiem” ludzi i modeli.
Możemy spodziewać się zachodzącej na naszych oczach zmiany roli matematyka? Zapewne. Wszak coraz częściej matematyk może pełnić rolę:
- projektanta eksperymentu (jak przeszukiwać przestrzeń rozwiązań),
- kuratora hipotez,
- i redaktora formalnych dowodów, a nie wyłącznie „samotnego autora” całego wywodu.
A zatem – czy AI rozwiązała już „nierozwiązywalne” tezy?
Na tym etapie uczciwa odpowiedź brzmi: AI nie rozwiązała jeszcze największych, klasycznych problemów milenijnych, ale zaczęła realnie wpływać na matematykę na trzech frontach:
- odkrywanie nowych konstrukcji i algorytmów (FunSearch, AlphaTensor),
- rozwiązywanie trudnych problemów i dowodzenie na poziomie olimpijskim (AlphaGeometry i kolejne systemy),
- przyspieszanie formalizacji i domykanie rozproszonych wyników (fala wokół problemów Erdősa + proof assistants).
Największa zmiana może więc nie polegać na tym, że „AI zastąpi matematyków”, tylko że matematyka zaczyna działać jak inżynieria: z automatyczną weryfikacją, iteracją i eksploracją na skalę, której człowiek sam nie udźwignie.
