Dobry dowód, to taki, który czyni nas mądrzejszymi.
Jurij Manin
Ledwie dwa lata temu zespół Google DeepMind chwalił się, że jego systemy sztucznej inteligencji osiągają wyniki na poziomie srebrnego medalu Międzynarodowej Olimpiady Matematycznej. Rok temu był to już poziom złotego medalu[1]. W ostatnim miesiącu DeepMind (z polskim akcentem w osobie Henryka Michalewskiego) ogłosił, że AlphaProof Nexus autonomicznie rozwiązał 9 z 353 otwartych problemów Erdősa i rozstrzygnął 44 z 492 hipotez z bazy OEIS[2].
Doniesień tego rodzaju pojawia się tyle, że coraz częściej przyjmujemy je ze zobojętnieniem lub sceptycyzmem. Nigdy nie brakuje komentarzy, że agent AI rozprawił się tylko z wybranym wariantem danego problemu i to tym najłatwiejszym. Albo że rozwiązany problem pozostawał otwarty tylko przez swoją niszowość i bałagan, a tak w ogóle to jest nieistotny.
Jednak nawet jeżeli takie uwagi są słuszne, nie zmienia to najważniejszego: przekroczyliśmy pewną granicę. Maszyna jest już w stanie nie tylko rozwiązać zadanie na poziomie prestiżowego konkursu, ale również wyjść poza dobrze poznany horyzont wiedzy. Nawet jeżeli narzędzia AI nie potrafią jeszcze dokonać przewrotu na miarę Medalu Fieldsa, ich rola rośnie w zastraszającym tempie. Tylko głupiec mógłby to ignorować.
W tej atmosferze holenderskie Centrum Lorentza przy Uniwersytecie w Lejdzie zorganizowało konferencję pod tytułem Mechanizacja i badania matematyczne z udziałem matematyków, informatyków i filozofów z dziesięciu państw. Wydarzenie doprowadziło do zawiązania szesnastoosobowej grupy roboczej (z kolejnym polskim akcentem: Bartoszem Naskręckim z UAM), która 2 czerwca 2026 roku opublikowała Deklarację z Lejdy w sprawie sztucznej inteligencji i matematyki.
Dokument wymienia pięć potencjalnych zagrożeń o „nieproporcjonalnie dużym wpływie” na młodych matematyków, a tym samym na długoterminową przyszłość królowej nauk. W największym możliwym skrócie, autorzy obawiają się:
Przeczytałem całość deklaracji i od razu powiem, że wbrew pozorom nie jest to antytechnologiczny manifest ani histeryczna petycja o zablokowanie ChataGPT na uczelniach. Autorzy nie próbują zawracać kijem Renu[3]. Już w preambule przyznają, że rozwijane technologie mogą rozpocząć nowy rozdział w historii matematyki. Pozostawiają swoim kolegom pełną swobodę w zakresie tego, czy i w jakim stopniu będą wykorzystywać dostępne narzędzia do swoich badań.
Jednocześnie sygnatariusze ostrzegają, że bez żadnej reakcji środowiska naukowego, matematyce grozi zawalenie się pod własnym ciężarem. Dlatego apelują o pilne ustalenie jasnych reguł gry, przystających do nowej rzeczywistości.
Oto na czym polega kłopot. Bez względu na to, czy mamy do czynienia z przebłyskiem ludzkiego geniuszu, natchnieniem zesłanym przez boginię Namagiri[4], czy wytworem LLM-u – konieczny jest dowód. Przy czym dowód dla matematyka jest czymś więcej niż tylko przekonującym argumentem. To misterna konstrukcja osadzona na fundamencie logiki.
Jeżeli wyobrazimy sobie twierdzenie jako świeżo odkrytą wysepkę, to dowód będzie prowadzącym do niej mostem. Jeżeli dowód jest poprawny, każda inna osoba, która przejdzie po tym moście, deska po desce, powinna dotrzeć do tego samego miejsca i zobaczyć to samo, co my.
Koncepcja dowodu daje matematykom dwie rzeczy, jakich nie zagwarantuje im żadna inna metoda poznawcza. Po pierwsze, najwyższy dostępny stopień pewności[5]. Skoro tak stanowi dowód, to twierdzenie musi być prawdziwe, bo inaczej zawali się logika. Po drugie, dowód daje zrozumienie. Nie mówi tylko, że coś jest prawdą albo fałszem, lecz wyjaśnia, dlaczego jest prawdą albo fałszem.
Cały szkopuł w tym, że nasz metaforyczny most może być kręty i długi. Oczywiście, istnieją dowody (np. niewymierności √2 albo wzoru na sumę kolejnych liczb naturalnych), które można zmieścić na połowie kartki.
Ale to tylko jedna strona matematyki. Dowód Wielkiego Twierdzenia Fermata, który sam w sobie można zapisać w paru linijkach, zajął Andrew Wilesowi i Richardowi Taylorowi ponad sto stron. Dowód twierdzenia Feita-Thompsona o grupach nieparzystego rzędu liczył około 255 stron. Nie wspominam już o skrajnym (i trochę kontrowersyjnym[6]) dowodzie twierdzenia o czterech kolorach, który zaowocował monografią długą na ponad 700 stron.
Mając to w głowie, spójrzmy na pierwsze i chyba najważniejsze z zagrożeń, wymienionych w Deklaracji Lejdejskiej:
Obecne techniki automatyzacji mogą generować wiarygodnie wyglądające, ale zawodne (a nawet błędne) argumenty, które trudno odróżnić od poprawnych dowodów matematycznych. Dotyczy to nie tylko argumentacji nieformalnej, ale także formalizacji, gdzie trudność polega na przełożeniu pojęć zapisanych w języku komputera na ich ludzkie przedstawienie. Te dynamiczne zmiany wywierają coraz większą presję na obecny system weryfikacji, zagrażając naszej zdolności do utrzymania tradycyjnych standardów poprawności, przejrzystości i niezależnej weryfikowalności dowodów.
Mamy dostęp do maszyny, która bez grymaszenia udzieli odpowiedzi na zadane pytanie, wypluwając mnóstwo mądrze wyglądającej treści. Szybko i śmiesznie niskim kosztem.
Czego nie mamy? Równie szybkiego i taniego systemu weryfikacji.
Rzućcie na biurko redaktora czasopisma naukowego sto artykułów. Z wierzchu każdy wygląda poważnie – zawiera twierdzenia, lematy[7], odniesienia, załączniki i tak dalej. Najwyżej dziesięć z tych prac jest naprawdę porządna i wartościowa. Czterdzieści jest poprawna, ale mało istotna dla dziedziny. Pozostałe pięćdziesiąt skrywa subtelne błędy, powtórzenia, źle przypisane idee albo argumenty, które rozpadają się po tygodniu sprawdzania przez specjalistę.
Tak to wyglądało kiedyś. Teraz na biurko redaktora trafia tysiąc tekstów, bo ich napisanie stało się łatwiejsze niż kiedykolwiek. Czy w ten sposób wzrasta ilość wiedzy? Być może. Czy wzrasta ilość pracy potrzebnej do odsiania śmieci? Z całą pewnością. Mówimy bowiem o artykułach ocierających się o granicę wiedzy, których sprawdzenie wymaga specjalisty znającego literaturę, rozumiejącego kontekst i potrafiącego wychwycić drobną pomyłkę ukrytą w jednej linijce na czterdziestej drugiej stronie obliczeń.
Pomyłkę albo halucynację.
Oczywiście, technologia działa w obie strony. Maszyna, która pomaga produkować matematyczną makulaturę, może też pomagać w jej odsiewaniu. Systemy takie jak Lean, Coq czy Isabelle już teraz pełnią ważną rolę w formalnym weryfikowaniu dowodów krok po kroku. Jednak nawet one nie rozwiązują całego problemu. Końcowym adresatem odkrycia nadal pozostaje matematyk z krwi i kości. To człowiek musi ocenić, czy wynik jest istotny, nowatorski, sensowny i przede wszystkim zrozumiały. Sama poprawność w granicach przyjętych definicji i aksjomatów to za mało, żeby rozwijać naukę.
System zaczyna się zatykać już teraz. Dotyczy to zresztą wszystkich dziedzin. Niedawno NeurIPS poinformowało o odrzuceniu 18,4% nadesłanych esejów i polemik jako wygenerowanych przez AI. Kolejne 12,7% zostało wstrzymanych z żądaniem przedstawienia dowodów na autorstwo człowieka. Nie wiem czy w tej sytuacji bardziej ironiczny jest fakt, że chodzi o artykuły poświęcone sieciom neuronowym i sztucznej inteligencji, czy to, że decyzję oparto na analizie – a jakże – automatycznego detektora.
Pojawia się wreszcie pytanie, jak odróżnić badacza, który wspiera się LLM-em w dobrej wierze, od cwaniaka bezwstydnie nabijającego sobie punkty. Ilka Agricola z Międzynarodowej Unii Matematycznej w swoim komentarzu do deklaracji pisze o zalewie „fałszywych prac, które mają jedynie zostać opublikowane i cytowane, a nie faktycznie przeczytane”.
Zwyczajowa punktoza, spotęgowana narzędziami do hurtowego generowania treści, może więc doprowadzić nie tylko do paraliżu, ale również do skażenia obiegu wiedzy na nieznaną dotąd skalę.
Wydaje się, że wzrost patonauki jest już nieunikniony, ale można i trzeba próbować minimalizować straty. Dlatego autorzy deklaracji wysuwają szereg rekomendacji pod adresem uczelni, instytucji, polityków oraz samych matematyków.
Przede wszystkim żądają pełnej transparentności. Każda nowa publikacja powinna zawierać osobną sekcję, podobną do bibliografii, w której naukowcy obligatoryjnie ujawnialiby listę wykorzystanych narzędzi oraz zasobów obliczeniowych. Organizacje i wydawnictwa miałyby pełne prawo egzekwować ten rygor i pilnować formalnej weryfikacji. Jak również zwiększyć nacisk na poszanowanie praw autorskich podczas treningu modeli językowych.
Skoro już jesteśmy przy autorstwie, to deklaracja stoi na stanowisku, że odkryć wciąż dokonują ludzie i nie należy przypisywać ich programom czy maszynom. Działa to jednak w obie strony: człowiek zyskuje uznanie, ale na nim spoczywa też pełna odpowiedzialność zarówno za poprawność tego, co z pomocą AI stworzył, jak i za prawidłowość cytowań oraz całej reszty.
Nie wydaje mi się, żeby proponowane wytyczne były szczególnie wygórowane czy idealistyczne. Powiedziałbym raczej, że to absolutne minimum, konieczne do zachowania elementarnej higieny poznawczej. Bez niej odkrycie naukowe przypomina pokaz iluzjonisty, który po przecięciu asystentki na pół, odmawia pokazania wnętrza skrzyni.
Duże wydawnictwa i organizacje już poczyniły pierwsze kroki w celu uzdrowienia sytuacji. Towarzystwo Matematyki Przemysłowej i Stosowanej zastrzegło niedawno, że autorzy powinni być zdolni bezpośrednio obronić każdy element zgłoszonego tekstu. Jeśli korzystali z AI, muszą to ujawnić i jasno oświadczyć, że biorą pełną odpowiedzialność za treść. Londyńskie Towarzystwo Matematyczne, podobnie, każe deklarować użycie AI przy generowaniu pomysłów, wykonywaniu obliczeń, weryfikowaniu dowodów, a nawet poprawianiu języka. Również Elsevier, jedno z największych wydawnictw naukowych na świecie, wymaga już oświadczeń o wykorzystaniu generatywnej AI.
Podpisy pod dokumentem złożyło do tego momentu ponad 2700 naukowców z całego świata. Obyśmy wkrótce doczekali się podobnych ruchów obejmujących wszystkie dyscypliny.
Ostatnie komentarze: