Matematycy oddają swoje twierdzenia pod lupę AI. Rewolucja w weryfikacji dowodów

Wkraczamy w erę, w której matematyczna pewność przestaje zależeć od subiektywnej oceny recenzenta, a zaczyna opierać się na bezlitosnej logice algorytmu. Narzędzia takie jak Lean czy Coq nie ulegają zmęczeniu i nie dają się uwieść autorytetowi autora, analizując każdy fragment dowodu z precyzją niedostępną dla człowieka. To fundamentalna zmiana paradygmatu, która przekształca samotną pracę geniusza w transparentny i weryfikowalny projekt inżynierski.

Teraz do gry wchodzą programy, które czytają dowody linijka po linijce.

Specjalistyczne narzędzia komputerowe, takie jak Lean czy Coq, potrafią sprawdzić każdy krok rozumowania z uporem, którego nie wytrzymałby żaden człowiek. W efekcie zmienia się nie tylko tempo badań, ale też samo pojęcie „pewności” w matematyce.

Od samotnego geniusza do zespołu pracującego w jednym repozytorium

Przez wieki proces wyglądał podobnie: badacz wymyślał twierdzenie, konstruował dowód, a potem latami czekał, aż inni eksperci go sprawdzą. Im trudniejszy temat, tym mniejsza grupa osób w ogóle potrafiła go zrozumieć, nie mówiąc o dokładnym przejrzeniu każdego szczegółu.

Przykładem jest Peter Scholze, jeden z najbardziej znanych współczesnych matematyków, laureat medalu Fields. W 2018 roku opublikował skomplikowane twierdzenie dotyczące tzw. przestrzeni skondensowanych. Dowód liczył setki stron i dotyczył obszaru tak abstrakcyjnego, że realnie kilka–kilkanaście osób na świecie mogło przejść go krok po kroku.

Sam autor nie spał spokojnie. Bał się, że gdzieś w gąszczu szczegółów ukrywa się błąd, którego żaden recenzent nie zdoła wyłapać.

Eksperyment, który stał się symbolem nowej epoki

Zamiast prosić o kolejne tradycyjne recenzje, Scholze ogłosił publiczne wyzwanie. Uruchomił projekt nazwany Liquid Tensor Experiment i zaprosił matematyków oraz informatyków, którzy znają system Lean, aby przepisali jego dowód na język zrozumiały dla programu.

Lean to tzw. asystent dowodów: oprogramowanie, które wymusza zapis rozumowania w formie absolutnie precyzyjnego kodu. Jeśli choć jeden krok logicznie nie wynika z poprzednich, system natychmiast blokuje dalszą pracę.

W projekt zaangażowała się międzynarodowa grupa badaczy. Przez kilka miesięcy tłumaczyli fragment po fragmencie, zamieniając pojęcia z wysoko abstrakcyjnej teorii na obiekty i reguły zrozumiałe dla programu.

Po około pół roku maszyna „przebiegła” po 180 tysiącach linii kodu opisujących całą konstrukcję. Żadnych sprzeczności. Żadnego kroku, którego nie dałoby się uzasadnić na podstawie wcześniejszych założeń. Scholze dostał odpowiedź, jakiej nie dałby mu żaden najbardziej życzliwy komitet recenzentów: tak, dowód jest spójny w każdym detalu.

Dla środowiska sygnał był jasny: oto pojawiło się narzędzie, które pozwala zastąpić wieloletnie, niepewne recenzowanie formalną kontrolą na poziomie pojedynczych symboli.

Asystenci dowodów zmieniają projekty „niemożliwe” w normalne zadania

Inna głośna historia dotyczy Maryny Viazovskiej, która rozwiązała słynną zagadkę o najgęstszym upakowaniu kul w ośmiu wymiarach. Samo sformułowanie problemu brzmi jak science fiction, a dowód – choć niezwykle elegancki – zawiera fragmenty tak techniczne, że ich kompletne ręczne sprawdzenie zajęłoby lata całym zespołom specjalistów.

Grupa matematyków postanowiła przenieść ten materiał do Lean. Projekt trwał miesiącami, obejmował współpracę osób rozrzuconych po uczelniach na kilku kontynentach. Finał: w 2024 roku pełny kod trafił na GitHub, a wraz z nim formalna gwarancja poprawności całego rozumowania.

Maszyna nie „wierzy” w autorytet laureatki medalu Fields. Albo każdy krok wynika z poprzednich, albo w którymś miejscu pojawia się czerwony komunikat błędu. Tu błędów nie było.

Największa zmiana dotyczy skali. Wcześniej wiele ambitnych projektów lądowało w szufladzie, bo sam proces recenzowania wydawał się niewykonalny. Setki stron specjalistycznych rachunków, dziesiątki przejść między teoriami – to za dużo na klasyczne „czytanie po kolei”. Teraz takie zadania stają się po prostu dużymi, ale możliwymi projektami inżynierskimi.

Biblioteka, która rośnie jak open source

Sercem ekosystemu Lean jest Mathlib – ogromna biblioteka definicji, twierdzeń i gotowych lem, z których można korzystać jak z klocków LEGO. Zawiera już ponad milion linii formalnej matematyki: od podstaw algebry po zaawansowane konstrukcje z najnowszych badań.

Każda nowa praca, którą ktoś sformalizuje, wzbogaca tę bazę. Następni badacze nie muszą zaczynać od zera, tylko sięgają po gotowe moduły: struktury, twierdzenia, całe teorie. W efekcie budowanie kolejnych dowodów zaczyna przypominać programowanie z użyciem dobrze utrzymanego frameworka.

• łatwiej dzielić duże problemy na mniejsze zadania dla różnych osób,
• ryzyko „przeoczenia drobiazgu” drastycznie spada,
• raz formalnie opisane narzędzia można ponownie wykorzystać w innych projektach,
• praca wielu osób z różnych uczelni naturalnie się łączy.

Maszyna wyłapuje błędy, które przeszły przez ludzkie recenzje

Ważny argument zwolenników formalizacji brzmi: takie systemy nie tylko potwierdzają poprawne dowody, lecz także znajdują pomyłki w pracach uznanych za wzorcowe. Kilka lat temu badacze przełożyli do Lean twierdzenie, za które przyznano prestiżową nagrodę. Podczas tego procesu program zatrzymał się w połowie – jedna z przejściowych lem nie wynikała logicznie z wcześniejszych założeń.

Autorzy musieli przeredagować fragment rozumowania. Przyznali, że żaden recenzent nie zwrócił na to uwagi. Nie chodziło o spektakularną katastrofę, raczej o brakujący argument, nad którym człowiek machnął ręką, wierząc w intuicję autora. Dla maszyny taka „droga na skróty” nie wchodzi w grę.

Asystent dowodów nie zmęczy się, nie zgubi wątku, nie zadowoli się ogólnym zarysem argumentu. Wymusza pełną przejrzystość każdego kroku.

Taka bezwzględna konsekwencja zmienia standardy jakości. Tam, gdzie dawniej wystarczało przekonujące wyjaśnienie i reputacja autora, dziś coraz częściej pada pytanie: „Czy ktoś to już sformalizował w Lean albo innym systemie?”.

Próg wejścia maleje dzięki AI

Przez długi czas tego typu narzędzia pozostawały domeną wąskiej grupy informatyków teoretycznych. Składnia była surowa, dokumentacja – techniczna, a sama praca przypominała pisanie kodu w egzotycznym języku. Dla wielu matematyków była to bariera nie do przeskoczenia.

Sytuacja szybko się zmienia. Coraz lepsze interfejsy, integracja z edytorami kodu i wsparcie ze strony modeli językowych sprawiają, że proces formalizacji przypomina interaktywną rozmowę z asystentem. Badacz pisze fragment dowodu w stylu „ludzkim”, a system podpowiada, jak zamienić go na poprawne konstrukcje w Lean, sugeruje brakujące kroki, czasem sam proponuje strukturę całego argumentu.

Co ta zmiana oznacza dla przyszłości matematyki

Rosnąca rola systemów takich jak Lean czy Isabelle rodzi szereg pytań. Czy młodzi badacze będą musieli od razu uczyć się formalizacji, tak jak dziś niemal każdy naukowiec musi znać podstawy programowania? Czy recenzje artykułów bez komputerowej weryfikacji stopniowo stracą na znaczeniu?

Na razie widać inny trend: matematycy korzystają z tych narzędzi tam, gdzie stawka jest wysoka, a dowody są bardzo złożone. Intuicja, wyczucie struktur i pomysły nadal należą do ludzi. Asystent przejmuje etap, który dla człowieka jest koszmarnie żmudny: upewnianie się, że w długim łańcuchu rozumowań nie wkradła się najmniejsza nielogiczność.

Dla studentów i doktorantów formalizacja staje się też ciekawym sposobem nauki. Zmusza do pełnego zrozumienia, jakie założenia są faktycznie używane w każdym kroku dowodu, gdzie potrzebna jest dodatkowa lema, a gdzie intuicja „czuje” więcej niż naprawdę wynika z rachunków. To wymagające, ale bardzo rozwijające ćwiczenie w precyzyjnym myśleniu.

Jeśli trend się utrzyma, część najważniejszych twierdzeń naszej epoki trafi nie tylko na łamy czasopism, lecz także do publicznie dostępnych repozytoriów zformalizowanego kodu. Każdy będzie mógł zobaczyć, jak dokładnie wygląda ścieżka od aksjomatów do finalnego wniosku – bez skrótów, narracyjnych ułatwień i „magicznych” przeskoków. To może nieco odebrać romantyzmu wizji samotnego geniusza, ale znacząco zwiększa zaufanie do tego, co matematycy uznają za prawdę.