Kiedy AI robi matematykę: debata o przyszłości dyscypliny

W ciągu ostatnich dwóch lat systemy AI osiągnęły złote medale na Olimpiadzie Matematycznej, autonomicznie wyprodukowały wyniki badawcze na poziomie doktoratu i obaliły hipotezy w geometrii kombinatorycznej. Te osiągnięcia uruchomiły w środowisku matematycznym debatę fundamentalną — nie tylko o możliwościach AI, ale o tym, czym jest matematyka i czy zachowuje swój sens bez ludzkiego wysiłku poznawczego.

Najważniejsze w skrócie

Systemy Google DeepMind i OpenAI osiągnęły poziom złotego medalu na Olimpiadzie Matematycznej (lato 2024)
Aletheia (Google DeepMind) autonomicznie wyprodukowała wyniki badawcze na poziomie Ph.D. w geometrii arytmetycznej
AI od OpenAI obaliło hipotezę w geometrii kombinatorycznej — wynik godny publikacji w czołowym piśmie matematycznym
Agent Gauss (Math, Inc.) sformalizował nagrodzony Medalem Fieldsa dowód Viazovskiej; 24-wymiarowy przypadek — samodzielnie w 2 tygodnie
Na 12. Forum Laureatów w Heidelbergu (wrzesień 2025) prognozy o AI wywołały palpabilny niepokój wśród młodych matematyków

Od papugi do rozumowania matematycznego

Przez dekady komputer był w matematyce narzędziem obliczeniowym, nie intelektualnym. W 1976 roku maszyny dowiodły twierdzenia o czterech barwach, sprawdzając 1936 przypadków — kontrowersyjnie, bo w sposób niemożliwy do zweryfikowania przez człowieka. Mimo to rola matematyka pozostawała centralna: człowiek formułował hipotezy, wyznaczał strategię i weryfikował rozumowanie. To równanie zmienia się gwałtownie.

Duże modele językowe (LLMs), opisywane jeszcze niedawno jako „stochastic parrots” zdolne jedynie do odtwarzania wzorców z internetu, stały się zaawansowanymi systemami do rozumowania matematycznego. Latem 2024 roku systemy od Google DeepMind i OpenAI osiągnęły wyniki równoważne złotemu medalowi na Międzynarodowej Olimpiadzie Matematycznej (IMO) — zawodach, w których zawodnicy rozwiązują sześć trudnych problemów z różnych dziedzin matematyki w ciągu dwóch dni.

Eksperymentalny system Google DeepMind o nazwie Aletheia poszedł dalej: autonomicznie wytworzył wyniki badawcze kwalifikujące się do publikacji na poziomie Ph.D. w geometrii arytmetycznej — obliczenia stałych struktury w dziedzinie abstrakcyjnej nawet dla większości matematyków. Znaczenie tego osiągnięcia tkwi nie w tematyce, ale w charakterze wykazanego rozumowania: samodzielne postawienie i rozwiązanie otwartego problemu naukowego. Niemal równocześnie system AI od OpenAI obaliło istotną hipotezę w geometrii kombinatorycznej. Czołowi matematycy potwierdzili, że wynik zasługiwałby na druk w prestiżowym piśmie, gdyby autorem był człowiek.

Agent Gauss i granica formalizacji

Równoległy kierunek zmian dotyczy połączenia LLMs z asystentami dowodów — systemami takimi jak Isabelle, Lean czy Rocq — które weryfikują poprawność logiczną każdego kroku rozumowania. Dotychczas tłumaczenie nieformalnego dowodu na kod rozumiany przez maszynę (tzw. formalizacja) było procesem ręcznym i żmudnym. Teraz AI zaczyna tę barierę usuwać.

W lutym 2025 roku firma Math, Inc. użyła agenta rozumowania o nazwie Gauss do sformalizowania dowodu, za który Maryna Viazovska z EPFL w Szwajcarii otrzymała Medal Fieldsa w 2022 roku. Viazovska rozwiązała problem optymalnego upakowania kul w 8 wymiarach. Gauss najpierw wspomagał matematyków przy formalizacji tego przypadku w ciągu kilku dni, a następnie autonomicznie sformalizował znacznie trudniejszy przypadek 24-wymiarowy w ciągu dwóch tygodni.

Gdyby nie ta warstwa formalnej weryfikacji, otwieranie projektów bez zabezpieczeń byłoby katastrofą. Ale w matematyce możemy całkowicie sprawdzić wyniki.

Terence Tao, profesor UCLA i medalista Fieldsa, o formalizacji jako fundamencie przyszłej współpracy matematycznej.

Heidelberg 2025: lęk egzystencjalny

We wrześniu 2025 roku, podczas 12. Forum Laureatów w Heidelbergu — corocznej konferencji skupiającej setki młodych matematyków przy ich intelektualnych idolach — AI zdominowało rozmowy od pierwszego dnia. Yang-Hui He z London Institute for Mathematical Sciences wyartykułował prognozę, która utkwiła w pamięci uczestników: jeśli AI przejmie formułowanie hipotez, przeszukiwanie przestrzeni dowodów i weryfikację wyników bez udziału człowieka, matematycy mogliby stać się „kapłanami wyroczni”.

Sala zareagowała niepokojem. Trill White, studentka z Deakin University w Australii, opisywała swoje myśli tamtego dnia: „To dewastujące. Co ludzie będą wnosić do matematyki? Czy stanie się ona czymś, czego nikt nie rozumie?” Jessica Randall z Google Developer Groups mówiła o „zbiorowym egzystencjalnym lęku” wśród młodych uczestników. Poczucie to było powszechne: uczestnicy uświadamiali sobie, że AI ma potencjał, by zastąpić ich w pracy, do której się szkolili.

Nie wszyscy reagują paniką. Jeremy Avigad z Carnegie Mellon University ujął pragmatyczne stanowisko krótko: matematycy są zainteresowani odpowiedziami na najtrudniejsze pytania matematyki, bez względu na to, kto lub co na nie odpowie. Część uznanych badaczy, w tym Yang-Hui He, jest komfortowa z tym, że AI przejmuje zadania dotychczas zastrzeżone dla człowieka.

Trzy wizje przyszłości

Z debaty wyłaniają się trzy stanowiska. Pierwsze to AI jako narzędzie — kalkulator dla matematyki wyższej, gdzie ludzkie rozumienie pozostaje nadrzędne. Akshay Venkatesh, medalista Fieldsa z Princeton, argumentuje, że matematyka służy nie tylko produkowaniu prawdziwych twierdzeń, ale też budowaniu wspólnego rozumienia. Maia Fraser z University of Ottawa dodaje, że dowód piękny i zrozumiały dla człowieka ma wartość niezależnie od tego, czy AI znajdzie swój własny.

Drugie stanowisko to współpraca — wizja Terence'a Tao. Jego koncepcja „big mathematics” zakłada ogromne, zdecentralizowane współprace ludzi i maszyn, gdzie AI wykonuje techniczny ciężar pracy, a ludzie zachowują aspekty kreatywne. Trzecie stanowisko, wywołujące największy opór, to AI jako wyrocznia: w pełni autonomiczny badacz, dla którego wyniki są ważniejsze niż ludzki proces ich odkrywania.

Dlaczego to ważne?

AI wkraczające w matematykę to nie tylko zmiana narzędzi — to wyzwanie epistemologiczne. Dowód niezrozumiały przez człowieka stawia pytanie, czy jest on tym samym rodzajem wiedzy co dowód, który można prześledzić krok po kroku. Środowisko matematyczne, choć podzielone co do wizji przyszłości, jest zgodne w jednym: AI ma potencjał transformacyjny, a jego kierunek zależy od decyzji podejmowanych teraz. Matematycy piszą eseje, organizują warsztaty i budują pierwsze wytyczne etyczne — stosując do AI tę samą precyzję, którą stosują do twierdzeń.

Ryzyko intelektualnej atrofii następnego pokolenia — jeśli studenci nauczą się omijać walkę z trudnym problemem — jest traktowane poważnie. Podobnie dostępność: jeśli matematyka będzie wymagać drogich modeli własnościowych, stanie się domeną wyłącznie bogatych instytucji. Stawką jest nie tylko status zawodu, ale charakter jednej z fundamentalnych dziedzin ludzkiej myśli.

Co dalej?

Formalizacja przez AI (projekty oparte na Lean i Rocq z asystentami LLM) będzie rozszerzać zakres samodzielnego wkładu maszyn — precedens Gaussa i dowodu Viazovskiej wyznacza kierunek
Sześć pozostałych Millennium Prize Problems stanie się kolejnym testem granicy możliwości AI: to najtrudniejsze otwarte problemy matematyki, z nagrodą miliona dolarów każdy
International Mathematical Union oraz środowiskowe grupy robocze przygotowują wytyczne dot. AI w publikacjach i badaniach — wyniki wpłyną na standardy finansowania i kryteria autorstwa