Matematycy oddają swoje dowody komputerom. Czy to koniec epoki kredy?

Coraz więcej matematyków prosi komputery, by te bezlitośnie prześwietliły ich najtrudniejsze twierdzenia linijka po linijce.

Przez tysiące lat wystarczały kartka, ołówek i kilka par ludzkich oczu. Teraz do zespołu dołącza nowy gracz: specjalne programy, które traktują każdy symbol w dowodzie jak fragment kodu i sprawdzają, czy cała konstrukcja naprawdę się trzyma.

Od samotnego geniusza do pracy ramię w ramię z maszyną

Klasyczny obraz matematyka jest prosty: ktoś siedzi sam w gabinecie, zapisuje kolejne strony i po miesiącach ogłasza efekt. Później inni eksperci powoli czytają dowód, szukając luk, przeoczeń, niedomówień. Czasem zajmuje to lata, a i tak zawsze pozostaje cień wątpliwości, czy naprawdę nikt niczego nie przeoczył.

Ten schemat zaczyna się kruszyć. Do gry weszły tzw. asystenci dowodów – programy takie jak Lean, Coq czy Isabelle. Matematycy przepisują swoje rozumowania do specjalnego języka, a maszyna sprawdza każdy krok z żelazną konsekwencją. Ani się nie męczy, ani nie traci koncentracji po setnej stronie.

Coraz więcej skomplikowanych twierdzeń przechodzi dziś przez etap „audytu” komputerowego, zanim trafi do podręczników i artykułów naukowych.

Słynny przypadek Petera Scholzego

Dobrym symbolem tej zmiany stała się historia Petera Scholzego, jednego z najbardziej znanych współczesnych matematyków, laureata medalu Fieldsa. W 2018 roku opublikował on gigantyczny, niezwykle abstrakcyjny dowód z teorii tzw. przestrzeni skondensowanych. Mówimy o setkach stron, które rozumie tylko garstka specjalistów na świecie.

Scholze nie czuł się jednak w pełni spokojny. Przy takiej skali łatwo przegapić subtelny błąd. Zamiast prosić kolejnych recenzentów o żmudne czytanie, zaproponował coś zupełnie innego: otwarty projekt, w którym społeczność matematyków spróbuje sformalizować jego pracę w systemie Lean. Akcja dostała nazwę Liquid Tensor Experiment.

Przez kilka miesięcy rozproszony po całym globie zespół przepisywał kolejne fragmenty dowodu na język zrozumiały dla programu. W sumie powstało około 180 tysięcy linii kodu. Gdy wszystko się złożyło, Lean przeszedł przez konstrukcję krok po kroku i nie znalazł żadnej luki logicznej. Scholze dostał potwierdzenie, jakiego nie jest w stanie dać żaden człowiek.

Gdy komputer bierze się za „niemożliwe” projekty

Najciekawsze w całej historii jest to, że takie formalne sprawdzanie otwiera drzwi do zadań, które wcześniej wydawały się po prostu nie do ogarnięcia. Nie dlatego, że matematycy nie umieli ich rozwiązać, ale dlatego, że pełna weryfikacja pochłonęłaby pół życia wielu osób.

Twierdzenia, których nikt nie chciał czytać do końca

Spektakularny przykład to praca Maryny Viazovskiej nad upakowaniem kul w ośmiu wymiarach. To jedno z klasycznych, wiekowych pytań: jak najgęściej „upchnąć” kule, tyle że w przestrzeni wymiarów więcej niż trzy. Jej dowód z 2016 roku był przełomem i przyniósł jej później medal Fieldsa. A zarazem – matematycznym koszmarem w lekturze.

Dowód miał fragmenty tak złożone, że skrupulatne przejście przez każdy techniczny szczegół ręcznie zajęłoby lata. Zespół badaczy zdecydował więc się przenieść całość do Lean. Przez wiele miesięcy budowali w systemie komplet narzędzi potrzebnych do opisania problemu, a następnie krok po kroku kodowali dowód Viazovskiej.

Efektem stał się obszerny projekt udostępniony na GitHubie. Program prześledził argument od początku do końca i zaakceptował go. To oznacza, że każda użyta własność, każde przekształcenie, każde założenie zostało jawnie zapisane i zgodne z rygorystycznymi zasadami logiki.

W takich przedsięwzięciach dużą rolę odgrywa Mathlib – ogromna biblioteka wiedzy zbudowana wokół Lean. Zawiera już ponad milion linii definicji, twierdzeń i gotowych narzędzi. Kolejne zespoły nie zaczynają od zera, tylko korzystają z tego, co zrobili poprzednicy. To trochę jak wspólna, rosnąca encyklopedia formalnych dowodów, na której można bezpiecznie się oprzeć.

• Lean, Coq, Isabelle – różne systemy, ten sam cel: sprawdzać dowody automatycznie.
• Mathlib – fundament Lean, wspólna biblioteka faktów matematycznych.
• GitHub – miejsce, gdzie zespoły udostępniają kod swoich formalnych dowodów.

Maszyna bez litości wobec ludzkich błędów

Nie chodzi jednak tylko o potwierdzanie poprawnych prac. Asystenci dowodów świetnie nadają się też do wyłapywania pomyłek, które wytrawni recenzenci potrafią przeoczyć.

Znany jest przypadek, gdy zespół matematyków przepisywał do Lean twierdzenie nagrodzone wcześniej prestiżową nagrodą. W pewnym momencie program zgłosił sprzeczność – coś w środku argumentu się nie domykało. Autorzy musieli przerobić fragment dowodu i dopisać brakujący element, przyznając, że żaden z recenzentów nie zauważył wcześniej luki.

Programy nie są „mądrzejsze” od ludzi, ale mają jedną przewagę: nie przymykają oka na skróty myślowe i nie domyślają się, co autor „miał na myśli”.

Człowiek, czytając tekst, często wypełnia luki intuicją. Maszyna tego nie robi. Jeżeli w kodzie brakuje konkretnego założenia, wszystko się sypie i system po prostu odmawia przejścia dalej. Z perspektywy nauki to duży plus, bo ogranicza ryzyko, że w literaturze zakorzeni się błąd, który potem latami trudno odkręcić.

Asystenci dowodów przestają być narzędziem tylko dla informatyków

Jeszcze kilka lat temu Lean czy Coq kojarzyły się głównie z informatyką teoretyczną. Trzeba było znać składnię, rozumieć sposób myślenia maszyny, radzić sobie z dość surowym interfejsem. Teraz pojawiają się nakładki wspierane przez AI, które tłumaczą „ludzką” matematykę na język formalny.

Duże modele językowe szkolone na kodzie Lean pomagają w generowaniu kolejnych kroków dowodu. Matematycy piszą szkic po swojemu, a asystent podpowiada, jak zamienić go w akceptowalny przez program zapis. To w praktyce obniża próg wejścia i przyciąga do formalnych dowodów osoby, które wcześniej trzymały się od nich z daleka.

Co to znaczy „udowodnić twierdzenie” w erze AI?

Cała ta zmiana ma też wymiar filozoficzny. Do niedawna za dowód uznawaliśmy elegancką, często dość zwartą argumentację, którą inteligentny czytelnik jest w stanie prześledzić od początku do końca. Formalizacja w Lean bywa niewyobrażalnie długa i techniczna – nikomu nie przyjdzie do głowy, by „po prostu ją przeczytać”.

W praktyce powstają więc dwie warstwy: dowód publikowany w tradycyjnej formie, zrozumiały dla ludzi, oraz jego rozpisana w najdrobniejsze szczegóły wersja maszynowa. Pierwsza daje intuicję i obraz całości, druga – stuprocentową pewność, że żadne ukryte założenie nie wymknęło się spod kontroli.

Dla części badaczy to naturalny krok naprzód: jak w inżynierii, gdzie skomplikowane konstrukcje przechodzą symulacje komputerowe, tak w matematyce skomplikowane twierdzenia przechodzą formalny audyt. Dla innych to lekkie przesunięcie akcentów – od piękna krótkiego argumentu ku technicznej pewności zapisanej w tysiącach linii kodu.

Co dalej: nowe zawody i nowe ryzyka

Jeśli trend się utrzyma, mogą pojawić się całkiem nowe role. Już teraz niektórzy młodzi badacze specjalizują się w formalizowaniu cudzych wyników. Potrafią szybko poruszać się w Lean, budować pomocnicze biblioteki, rozpisywać „ludzkie” twierdzenia tak, by zaakceptował je program. Taka umiejętność zaczyna mieć realną wartość na rynku akademickim i w firmach zajmujących się weryfikacją oprogramowania czy kryptografią.

Istnieje też ryzyko, że zbyt łatwo zaczniemy traktować maszynę jak nieomylne orzecznictwo. Programy działają poprawnie tak długo, jak długo poprawny jest ich własny kod oraz założenia na starcie. Jeżeli w Mathlib zakorzeni się kiedyś błąd na niskim poziomie, może on wpłynąć na wiele późniejszych formalnych dowodów. Dlatego zespoły pracujące nad tymi narzędziami przykładają ogromną wagę do testów i powolnego, przemyślanego rozwoju bibliotek.

Z perspektywy zwykłego czytelnika cała sprawa może brzmieć abstrakcyjnie, ale jej skutki łatwo sobie wyobrazić. Matematyka stoi u podstaw kryptografii, komunikacji satelitarnej, modeli klimatycznych, algorytmów w bankowości czy transporcie. Tam, gdzie stawką są miliardy złotych albo ludzkie bezpieczeństwo, argument w stylu „wszyscy eksperci przeczytali i nikt nie widzi błędu” staje się coraz mniej wystarczający. Znacznie lepiej mieć w ręku formalny certyfikat, że cała konstrukcja naprawdę jest logicznie spójna.

Razem z rozwojem AI rośnie więc nowy obszar: współpraca człowieka, który wymyśla twierdzenia i strategie, z maszyną, która pamięta wszystko, niczego nie zgaduje i cierpliwie dopina każdy szczegół. Matematyka, choć wciąż opiera się na ludzkiej intuicji, zaczyna działać w trybie, który bardziej przypomina inżynerię oprogramowania niż romantyczną wizję samotnego geniusza z tablicą i kredą.