Sztuczna inteligencja rozwiązuje coraz trudniejsze problemy matematyczne – i robi to z taką pewnością siebie, że nawet najlepsi matematycy świata zaczynają mieć wątpliwości, czy potrafią odróżnić poprawny dowód od przekonująco brzmiącego błędu. To nie scenariusz science fiction, lecz rzeczywistość, która zaczęła się materializować w 2025 roku podczas tajnego spotkania w Kalifornii.
Kilkadziesiąt czołowych nazwisk ze świata matematyki zebrało się, by przetestować model o4-mini od OpenAI. Wyniki były szokujące – nie dlatego, że AI rozwiązała wszystkie zadania bezbłędnie, ale dlatego, że jej odpowiedzi brzmiały jak wywód prawdziwego matematyka. Ken Ono, profesor teorii liczb z Uniwersytetu Wirginii, przyznał wprost: „I’ve never seen that kind of reasoning before in models. That’s what a scientist does.”
Ale Ono sam wskazał na paradoks: ten sam model „opanował proof by intimidation” – czyli udowadnianie przez zastraszenie. Mówi wszystko z taką pewnością siebie, że trudno mu się oprzeć, nawet kiedy się myli.
Jeśli chcesz otrzymać raport przed oficjalną premierą oraz zobaczyć nazwę swojej firmy wśród uczestników badania – zostaw adres email na końcu ankiety.
Kiedy pewność siebie staje się problemem
Przez stulecia matematyka opierała się na prostej zasadzie: przekonujący argument to dobry znak, bo tylko wybitny matematyk potrafi skonstruować naprawdę przekonujący dowód. AI tę zasadę całkowicie złamała.
Terry Tao, matematyk z UCLA i laureat Medalu Fieldsa z 2006 roku, ostrzega przed konsekwencjami:
„Unfortunately, the AI is much better at sounding like they have the right answer than actually getting it… right or wrong; they will always look convincing.”
Tao dodaje coś jeszcze bardziej niepokojącego: AI nauczona osiągania celów będzie „cheat like crazy” – czyli oszukiwać na wszelkie możliwe sposoby, żeby cel osiągnąć. W kontekście dowodów matematycznych oznacza to ryzyko produkowania setek wyglądających poprawnie argumentów, które w rzeczywistości zawierają ukryte błędy.
To nie jest problem czysto akademicki. Wyobraźmy sobie, że AI „udowadnia” coś w dziedzinie kryptografii – a my, zamiast sprawdzić dowód krok po kroku, po prostu mu ufamy.
Dowód jako konstrukt społeczny
Tu wchodzimy na grunt, który może zaskoczyć osoby spoza świata nauki. Matematyczny dowód nie jest absolutną prawdą wykutą w kamieniu – to w dużej mierze konstrukt społeczny.
Dowód uznaje się za prawdziwy wtedy, gdy wystarczająca liczba kompetentnych matematyków przeanalizuje go i uzna za poprawny. To oznacza, że powszechnie akceptowany dowód nie gwarantuje stuprocentowej pewności.
Doskonałym przykładem jest historia Andrew Wilesa i Ostatniego Twierdzenia Fermata. W 1993 roku Wiles ogłosił przed światem, że udowodnił problem, który przez 350 lat opierał się wszystkim próbom rozwiązania. Szampan był otwierany, gazety na całym świecie pisały o triumfie. I wtedy, podczas recenzji, odkryto poważny błąd. Wiles spędził kolejny rok na naprawianiu dowodu.
Andrew Granville z Uniwersytetu w Montrealu uważa, że podobne problemy mogą dotyczyć innych znanych dowodów – po cichu, bez rozgłosu.
Lean i formalna weryfikacja – ratunek czy zbytnia skomplikowanie?
Odpowiedzią środowiska matematycznego na ryzyko związane z AI jest rosnące zainteresowanie językami formalnej weryfikacji, z których najpopularniejszy to Lean.
Lean wymusza od matematyka przetłumaczenie dowodu na precyzyjny kod komputerowy. Każdy krok jest następnie sprawdzany maszynowo – jeśli cokolwiek nie gra logicznie, program odmawia przyjęcia argumentu. Nie ma miejsca na niejasności językowe, nie ma miejsca na „rozumie się samo przez się”.
Kevin Buzzard z Imperial College London, jeden z czołowych zwolenników tego podejścia, przyznaje, że zainteresował się formalną weryfikacją właśnie dlatego, że niepokoiły go niekompletne i niepoprawne ludzkie dowody. Teraz widzi w tym kombinacji AI i Lean ogromny potencjał:
„You would like to think that maybe we can get the system to not just write the model output, but translate it into Lean, run it through Lean.”
Tao zgadza się z tym kierunkiem: „If we force AI output to produce things in a formally verified language, then this, in principle, solves most of the problem.”
Brzmi jak gotowe rozwiązanie. Ale czy na pewno?
Komentarz Piotra Wolniewicza, Redaktora Naczelnego AIPORT.pl:
Czytając o tym, jak AI „opanowała proof by intimidation”, myślę o szerszym problemie, który dotyczy nas wszystkich – nie tylko matematyków. Coraz częściej akceptujemy odpowiedzi, bo brzmią pewnie i kompetentnie, a nie dlatego, że je zweryfikowaliśmy. To nie jest nowy problem AI – to odwieczna słabość ludzka. AI po prostu wyostrzyła ją do granic. Z jednej strony połączenie modeli językowych z systemami takimi jak Lean brzmi jak naprawdę dobre rozwiązanie – maszyna produkuje, maszyna weryfikuje, człowiek ocenia wynik. Ale zadaję sobie pytanie: jeśli coraz więcej etapów procesu poznawczego przenosimy na maszyny, to w którym miejscu matematyka przestaje być ludzką aktywnością? I czy to w ogóle zły kierunek – czy może po prostu nieuchronny?
Dowód, którego nikt nie rozumie
Formalna weryfikacja rozwiązuje jeden problem, ale otwiera inny, głębszy.
Jeżeli AI będzie w stanie samodzielnie – od postawienia hipotezy, przez testowanie, aż po weryfikację – udowodnić coś, czego żaden człowiek nie jest w stanie zrozumieć, to co z tym zrobić? Marc Lackenby z Uniwersytetu Oksfordzkiego mówi krótko: „You’ve proved something.” Ale dodaje zaraz pytanie, które trudno zignorować – jaki jest sens udowadniania czegoś, co pozostaje poza zasięgiem ludzkiego rozumienia?
Buzzard wskazuje, że ta sytuacja nie jest zupełnie nowa. Istnieją już dziś artykuły naukowe z dwudziestoma współautorami, z których każdy rozumie tylko swój fragment. Nikt nie ogarnia całości. I jakoś to działa.
Podobna historia dotyczy twierdzenia o czterech barwach – jednego z najsłynniejszych wyników w historii matematyki. Jego pierwsze komputerowo wspomagane dowody z lat 70. wywołały w środowisku matematycznym prawdziwe oburzenie. Dziś to zaakceptowany fakt w podręcznikach akademickich.
Warto przy tym wymienić przykłady problemów, przy których rozwiązaniu AI mogłaby odegrać kluczową rolę:
- P vs. NP – jeden z największych otwartych problemów matematyki, który dotyczy tego, czy problemy łatwe do zweryfikowania są też łatwe do rozwiązania; odpowiedź zrewolucjonizowałaby kryptografię, logistykę i odkrycia naukowe
- Hipoteza Riemanna – dotycząca rozkładu liczb pierwszych, otwarta od 1859 roku
- Równania Naviera-Stokesa – opisujące ruch płynów, kluczowe dla fizyki i inżynierii
Matematyka wchodzi w nieznane
Przez wieki dowodzenie i weryfikacja dowodów były działalnościami czysto ludzkimi – argumenty budowane były po to, by przekonać innych ludzi. To się zmienia.
Zbliżamy się do punktu, w którym maszyny mogą produkować hermetycznie szczelną logikę, potwierdzoną przez formalne systemy, której najlepsi matematycy świata nie będą w stanie samodzielnie prześledzić. Pytanie nie brzmi już „czy AI może robić matematykę” – brzmi „czy matematyka, którą robi AI, jest jeszcze matematyką w ludzkim sensie tego słowa.”
Na to pytanie nikt dziś nie zna odpowiedzi.
