Komputer sprawdza dowody szybciej niż profesor? Tak zmienia się matematyka

Przez tysiąclecia fundamentem matematyki była kartka papieru i subiektywna ocena drugiego człowieka, co często prowadziło do przeoczenia drobnych, lecz krytycznych błędów. Dziś stajemy u progu ery, w której asystenci dowodów tacy jak Lean stają się bezlitosnymi sędziami prawdy absolutnej, zdolnymi przemielić setki tysięcy linii kodu w poszukiwaniu logicznej luki. To nie tylko techniczna ciekawostka, ale fundamentalna zmiana, która przenosi ciężar dowodzenia z gabinetów samotnych geniuszy do otwartych, cyfrowych repozytoriów dostępnych dla każdego.

Przez tysiące lat wystarczały kartka, ołówek i cierpliwi recenzenci. Dziś do gry wchodzi oprogramowanie takie jak Lean, Coq czy Isabelle, które potrafi przemielić setki tysięcy linii formalnego zapisu i wychwycić błąd tam, gdzie ludzki umysł dawno by się poddał. To nie jest już ciekawostka dla informatyków, ale realna zmiana sposobu uprawiania matematyki.

Od samotnego geniusza do zespołu z komputerem w tle

Klasyczny obraz matematyka to ktoś zamknięty w gabinecie, pracujący samotnie nad kolejnymi równaniami. Ten model powoli się rozpada. Przykłady z ostatnich lat pokazują, że najtrudniejsze twierdzenia coraz częściej powstają i są weryfikowane w trybie kolektywnym – z aktywnym udziałem oprogramowania.

Dobrym symbolem tej zmiany jest historia jednego z najbardziej rozpoznawalnych młodych matematyków, laureata medalu Fields, który kilka lat temu ogłosił bardzo złożony wynik z zakresu tak zwanych przestrzeni skondensowanych. Dowód miał setki stron i dotyczył obszaru, którym zajmuje się garstka ekspertów na całym świecie. Nawet dla nich przejrzenie wszystkiego „na piechotę” było ekstremalnie trudne.

Zamiast czekać latami na pełną, ręczną weryfikację, uczony postanowił inaczej podejść do problemu. Ogłosił publiczny projekt, znany jako Liquid Tensor Experiment, w którym zaprosił społeczność do przepisania jego pracy na język systemu Lean – jednego z najbardziej zaawansowanych asystentów dowodów.

Lean jako bezlitosny korektor

Lean należy do klasy narzędzi zwanych asystentami dowodów (proof assistants). Ich zadanie jest proste w założeniu, a bezlitosne w praktyce: każdy krok rozumowania musi zostać zapisany w formalnym języku i spełnić ustalone reguły logiki. Jeśli choć jeden fragment się nie zgadza, program odmawia przejścia dalej.

W przypadku Liquid Tensor Experiment efekt był spektakularny. W ciągu kilku miesięcy międzynarodowy zespół matematyków i informatyków stworzył około 180 tysięcy linii kodu w Lean, które odpowiadały kolejnym elementom skomplikowanego dowodu. Program przeanalizował wszystko i nie znalazł żadnego logicznego pęknięcia. Dla autora oznaczało to poziom pewności niedostępny w tradycyjnym modelu recenzji.

Asystent dowodów nie ufa nazwisku, reputacji ani intuicji. Albo każdy krok jest logicznie poprawny, albo projekt po prostu się nie kompiluje.

Ta historia pokazała środowisku naukowemu, że komputer może pełnić rolę bezstronnego, niestrudzonego recenzenta, a przy okazji zmienić sposób organizacji pracy: od samotnej walki do wspólnego, rozproszonego projektu prowadzonego w otwartym repozytorium.

Projekty, które kiedyś były „zbyt duże”, stają się wykonalne

Kolejny przykład dotyczy jednego z najsłynniejszych problemów geometrii: jak najgęściej upakować kule w przestrzeni o wyższej liczbie wymiarów. W 2016 roku matematyczka Maryna Viazovska podała rozwiązanie dla wymiaru ósmego. Jej dowód, nagrodzony później medalem Fields, był niezwykle skondensowany i techniczny.

Dla klasycznego procesu recenzyjnego to koszmar: mała liczba ludzi na świecie potrafi go w pełni przeczytać, a jeszcze mniej ma czas, by to zrobić tak drobiazgowo, jak wymaga tego rygor matematyki. Stąd pomysł, by cały argument sformalizować w Lean i oddać do sprawdzenia maszynie.

Projekt okazał się trudny logistycznie. Zaangażował międzynarodową grupę specjalistów, którzy przez wiele miesięcy tłumaczyli poszczególne fragmenty pracy na język formalny. W 2024 roku gotowy kod trafił na GitHub – każdy chętny może zobaczyć, jak dokładnie zapisano te idee w postaci nadającej się do kontroli przez program.

To, co dla człowieka jest „jednym oczywistym krokiem”, dla komputera potrafi zamienić się w dziesiątki linii precyzyjnej logiki.

Takie projekty pokazują istotę rewolucji. Wcześniej wiele wielkich dowodów było moralnie przekonujących, ale technicznie tak rozbudowanych, że pełna, niezależna weryfikacja graniczyła z niemożliwością. Teraz oprogramowanie zmienia „zbyt wielkie” przedsięwzięcia w serie mniejszych zadań, które można zlecić grupie współpracowników, doktorantom, a nawet zaawansowanym amatorom.

Rosnące biblioteki wiedzy maszynowej

Sercem tego ekosystemu jest tak zwana Mathlib – centralna biblioteka Lean zawierająca formalne definicje, twierdzenia i dowody. Obecnie liczy już ponad 1,2 miliona linii, a jej zawartość rośnie niemal codziennie.

• zawiera podstawy algebry, analizy, teorii liczb i wielu innych działów,
• dzięki niej nowe projekty nie zaczynają od zera – korzystają z gotowej infrastruktury,
• każdy nowy dowód, raz wprowadzony, staje się klockiem, którym mogą posłużyć się inni.

Tworzy się w ten sposób swoisty „kod źródłowy matematyki”, z którego kolejne pokolenia badaczy mogą korzystać jak programiści z bibliotek open source. Różnica jest taka, że tutaj każda funkcja to precyzyjne twierdzenie, a każda zależność jest sprawdzona logicznie.

Maszyna wykrywa błędy w nagradzanych pracach

Asystenci dowodów nie tylko potwierdzają poprawność istniejących twierdzeń. Czasem psują dobre samopoczucie autorom, wyciągając na wierzch błędy, które umknęły wszystkim recenzentom. Znany jest przypadek pracy wyróżnionej prestiżową nagrodą, którą zespół próbował później sformalizować w Lean.

W trakcie tego procesu program wskazał, że w jednej z kluczowych części brakuje ważnej hipotezy. Logika się nie domykała. Autorzy musieli wrócić do argumentu i go przeredagować. Żaden z recenzentów, mimo dużego doświadczenia, nie wyłapał problemu wcześniej. Program – tak.

Maszyna nie przeoczy „drobnego założenia”, które autorowi wydaje się oczywiste, a recenzentowi umyka przy setnej stronie technicznych rachunków.

Dla części badaczy to niewygodne lustro, ale równocześnie narzędzie podnoszące standardy całej dyscypliny. Artykuł, którego pełną wersję da się bezbłędnie zrealizować w Lean czy Coq, zyskuje szczególną wagę: prawdopodobieństwo ukrytej luki maleje niemal do zera.

Od narzędzia dla informatyków do codziennej praktyki

Jeszcze dekadę temu obsługa asystentów dowodów wymagała biegłości programistycznej. Wielu matematyków odbijało się od skomplikowanej składni i surowego interfejsu. Dziś sytuacja się zmienia, również dzięki AI.

Modele językowe pomagają już przekładać szkice dowodów z tradycyjnego zapisu na kod formalny. Podpowiadają brakujące kroki, sugerują właściwe lematu czy twierdzenia z biblioteki Mathlib. Interfejsy stają się przyjaźniejsze, a naukowcy, którzy wcześniej nie programowali, zaczynają traktować te narzędzia jak rozszerzenie swojego warsztatu.

Coraz wyraźniej widać podział ról: kreatywność, intuicja i wybór kierunku badań po stronie człowieka, kontrola formalna i pamięć długoterminowa po stronie maszyny.

Co to oznacza dla przyszłych matematyków i dla nas wszystkich

Automatyzacja dowodów rodzi zarówno entuzjazm, jak i obawy. Część badaczy martwi się, że młode pokolenia za bardzo polegać będą na narzędziach, nie ucząc się „ręcznego” dowodzenia. Inni przypominają, że podobne lęki towarzyszyły wprowadzeniu kalkulatorów czy komputerów algebraicznych, a mimo to podstawowe umiejętności nie zniknęły, tylko zmienił się zakres tego, co uważa się za standard.

W praktyce asystenci dowodów mogą stać się dla studentów świetnym treningiem ścisłego myślenia. Program nie wybacza skrótów myślowych ani „to przecież oczywiste”, wymusza więc doprecyzowanie argumentu. Dobrze prowadzone zajęcia z Lean czy Coq mogą paradoksalnie poprawić warsztat logiczny, zamiast go rozmywać.

Konsekwencje sięgają także poza czystą matematykę. Formalnie zweryfikowane twierdzenia trafiają do inżynierii oprogramowania, kryptografii, projektowania układów scalonych. Błąd logiczny w tym obszarze to nie tylko akademicki problem, ale ryzyko dziury bezpieczeństwa, awarii systemu finansowego czy błędnego działania autonomicznego samochodu. Im więcej kluczowych fragmentów teorii przejdzie przez sito takich narzędzi jak Lean, tym solidniejsze fundamenty dostaną późniejsze technologie.

Dla osób spoza branży ta zmiana może wydawać się abstrakcyjna, ale ma bardzo przyziemny aspekt: jeśli za kilka lat bank, nawigacja w aucie czy system sterujący samolotem będą oparte na algorytmach, których własności udowodniono i zweryfikowano maszynowo, realnie wzrośnie nasze bezpieczeństwo. Matematyka, przechodząc na hybrydowy model współpracy z komputerami, zaczyna dostarczać nie tylko eleganckie równania, ale także mocniejsze gwarancje dla technologii, z których korzystamy codziennie.