Komputery sprawdzają dziś dowody twierdzeń. Matematycy mówią: to rewolucja

Matematycy coraz częściej proszą o pomoc nie kolegów po fachu, lecz… programy komputerowe.

Te bez litości wyłapują każdy błąd w dowodach.

Przez tysiące lat standardem był ołówek, papier i miesiące żmudnej weryfikacji przez wąskie grono ekspertów. Teraz na biurkach badaczy pojawiają się narzędzia takie jak Lean, Coq czy Isabelle, które przekładają dowody na kod i sprawdzają je linijka po linijce z dokładnością, jaka jest poza zasięgiem ludzkiej pamięci i koncentracji.

Od samotnika z kartką papieru do zespołów pracujących w jednym repozytorium

Klasyczny obraz matematyka to samotnik pochylony nad notesem, który latami dopracowuje jedną ideę. Ten model rodził arcydzieła, ale miał słabe strony: łatwo było coś przeoczyć, a weryfikacja gigantycznych dowodów potrafiła ciągnąć się całe dekady.

Dobrym symbolem zmiany stała się historia Petera Scholzego, jednego z najbardziej rozpoznawalnych współczesnych matematyków, laureata medalu Fieldsa. W 2018 roku opublikował rozbudowany, wysoce abstrakcyjny wynik dotyczący tzw. przestrzeni kondensowanych. Dowód liczył setki stron i dotykał obszaru, który rozumie garstka ekspertów na świecie.

Scholze nie był jednak w pełni spokojny. Obawiał się, że w gąszczu argumentów kryje się subtelny błąd, którego nie wyłapią żadni recenzenci. Zamiast szukać kolejnych ludzi gotowych miesiącami śledzić każdy krok, przeniósł sprawę do środowiska programistów i matematyków pracujących z Leanem. Tak narodził się projekt o nazwie Liquid Tensor Experiment.

Zadanie brzmiało prosto, choć wykonanie wymagało ogromnego wysiłku: przepisać cały dowód Scholzego do formalnego języka Lean, tak aby program mógł automatycznie sprawdzić logikę każdego kroku. Do projektu dołączyli specjaliści z różnych krajów, komunikując się przez internet i pracując równolegle na tych samych plikach kodu.

Po około pół roku powstał formalny zapis liczący około 180 tysięcy linii. Lean nie zgłosił żadnej niezgodności. Scholze uzyskał stopień pewności, którego nie dałby mu żaden ludzki recenzent.

Ta historia pokazała, że matematyka nie musi już opierać się na modelu samotnego geniusza, którego pracy bronią jedynie reputacja i opinia kilku autorytetów. Pojawia się coś w rodzaju „otwartego projektu matematycznego”, gdzie dziesiątki osób mogą równocześnie rozwijać formalny zapis jednego twierdzenia, a program czuwa nad spójnością całości.

Gdy potężne problemy stają się wykonalne dzięki formalizacji

W kolejnym głośnym przypadku narzędzia formalne wkroczyły w obszar bardzo trudnego, klasycznego problemu z geometrii. Maryna Viazovska rozwiązała koncepcję dotyczącą najgęstszego upakowania kul w ośmiowymiarnej przestrzeni – problem, który od wieków dręczył matematyków. Jej dowód, nagrodzony medalem Fieldsa, był gęsty, techniczny i niezwykle wymagający w szczegółowej kontroli.

Grupa badaczy postanowiła przełożyć cały ten materiał na kod w Leanie. W praktyce oznaczało to stworzenie komputerowej wersji każdego pojęcia, każdej funkcji i każdego kroku rozumowania. Po długich miesiącach pracy powstał kompletny projekt opublikowany w repozytorium GitHub – coś w rodzaju „mechanicznego potwierdzenia”, że konstrukcja Viazovskiej nie zawiera luk.

To nie jest pojedynczy przypadek, lecz zapowiedź nowego standardu. Do niedawna wiele imponujących twierdzeń budziło wątpliwości nie dlatego, że wydawały się fałszywe, lecz ze względu na niebotyczną długość i złożoność dowodów. Niewielka pomyłka lub brakująca hipoteza mogły czaić się gdzieś w środku, a znalezienie jej wymagałoby lat wytężonej lektury.

Dzięki narzędziom typu:

• Lean – popularny asystent dowodów rozwijany jako projekt open source,
• Coq – system stworzony pierwotnie przez informatyków zajmujących się weryfikacją oprogramowania,
• Isabelle – rozbudowane środowisko do logiki i matematyki formalnej,

takie gigantyczne projekty da się rozbić na tysiące drobnych kroków i rozdzielić między członków zespołu. Maszyna nie przyspiesza samego procesu twórczego, ale otwiera możliwość rzetelnego sprawdzenia tego, co wcześniej uchodziło za „zbyt duże, by je naprawdę przejrzeć”.

Rosnąca biblioteka gotowej matematyki

Serce Leana stanowi biblioteka Mathlib, w której zgromadzono już ponad milion linii formalnych definicji i twierdzeń. To coś w rodzaju ogromnego, matematycznego „systemu operacyjnego”. Nowy użytkownik nie musi zaczynać od zera, bo może korzystać z gotowych opisów liczb, struktur algebraicznych, topologii czy miary.

Im większa staje się ta baza, tym szybciej można formalizować kolejne wyniki. Badacz nie musi za każdym razem definiować od podstaw pojęć znanych od ponad stu lat, bo wystarczy sięgnąć do gotowych modułów.

Maszyna wyłapuje błędy, których nie dostrzegli recenzenci

Asystenty dowodów działają nie tylko jako „automatyczne pieczątki potwierdzające poprawność”. Zdarza się, że w trakcie przepisywania znanego twierdzenia do formalnego języka wychodzi na jaw, że gdzieś po drodze brakuje założenia albo pewien krok nie da się przeprowadzić bez dodatkowego argumentu.

W jednym z opisywanych przypadków grupa matematyków postanowiła sformalizować twierdzenie, za które autorzy dostali prestiżową nagrodę. Dowód przeszedł recenzje w wiodących czasopismach, więc wydawał się wzorcowo solidny. Kiedy jednak tłumaczono go linijka po linijce na zapis w Leanie, program zatrzymał się na konkretnym fragmencie – brakowało odpowiedniego ogniwa w łańcuchu wnioskowań.

Program nie „domyślił się”, co mieli na myśli autorzy. Zmuszał do dopisania brakującej części lub zmiany argumentu tak, aby dał się przeprowadzić w pełni formalnie.

To pokazuje, jak mocno różni się ludzka lektura od działania systemu formalnego. Recenzent, nawet bardzo uważny, często wypełnia luki intuicją: „tu autorzy na pewno mieli na myśli to i to, to jest oczywiste”. Maszyna nie przyjmuje takich założeń bez dowodu. Z punktu widzenia rygoru to ogromny zysk – ogranicza się ryzyko, że do literatury trafią prace z drobną, ale brzemienną w skutkach pomyłką.

Asystent dowodów jako narzędzie do nauki

Jeszcze kilka lat temu praca z Leanem czy Coqiem wymagała niemal pełnoprawnych umiejętności programistycznych. Dziś sytuacja się zmienia. Powstają interaktywne środowiska, wtyczki do popularnych edytorów i dodatki oparte na AI, które pomagają przekładać tradycyjne rozumowania na język formalny.

Coraz częściej uczelnie organizują kursy, w których studenci już na etapie magisterskim poznają podstawy formalizacji. System podpowiada im kolejne kroki, zaznacza niezgodności, sugeruje użycie istniejących lematów z biblioteki. Dla początkujących to sposób, by na własnej skórze zobaczyć, gdzie w ich argumentach brakuje precyzji.

Co się zmienia dla samej matematyki

Współpraca ludzi z systemami formalnymi rodzi kilka wyraźnych trendów. Po pierwsze, rośnie znaczenie dużych, zespołowych projektów, które przypominają bardziej rozwój oprogramowania niż klasyczne „samotne” badania. Po drugie, coraz wyraźniej rozdziela się rola twórcy idei i rola „inżyniera formalnego”, który potrafi opisać ją w kodzie.

Niektórzy matematycy zaczynają nawet projektować swoje argumenty od razu z myślą o formalizacji. Starają się unikać zbyt mętnych skrótów typu „oczywiste z definicji”, bo wiedzą, że później program będzie wymagał znacznie więcej szczegółów. Z czasem może to wpłynąć na styl pisania prac naukowych: zamiast bardzo lapidarnej formy pojawią się teksty od razu bliższe temu, co da się wrzucić do Leana.

Takie podejście niesie też praktyczne skutki poza czystą teorią. Algorytmy kryptograficzne, protokoły komunikacyjne czy fragmenty kodu sterującego infrastrukturą krytyczną już dziś bywają weryfikowane z wykorzystaniem narzędzi pokrewnych do systemów dowodzenia matematycznego. Im silniej matematyka przechodzi na język formalny, tym łatwiej przenosi się te same metody do inżynierii.

Dlaczego warto śledzić rozwój tej niszowej, ale wpływowej dziedziny

Na pierwszy rzut oka formalizacja dowodów wydaje się bardzo odległa od codzienności. Mało kogo interesuje, jak wygląda zapis słynnego twierdzenia w postaci tysięcy linii kodu. W tle toczy się jednak spór o to, czym właściwie staje się wiedza matematyczna w erze cyfrowej.

Jeżeli najważniejsze twierdzenia zaczniemy traktować jako obiekty formalne, które muszą istnieć w publicznym repozytorium i przechodzić automatyczną weryfikację, zmieni się też sposób dzielenia się wynikami, przyznawania nagród czy prowadzenia sporów naukowych. Zamiast dyskusji „czy recenzenci czegoś nie przeoczyli”, będzie raczej pytanie „czy projekt formalizacyjny został ukończony i przeszedł wszystkie testy”.

W dłuższej perspektywie narzędzia takie jak Lean mogą stać się dla matematyki tym, czym kompilator jest dla programisty: nie tylko mechanizmem sprawdzającym poprawność, ale też nieodłączną częścią samego procesu twórczego. A to znaczy, że przyszłe, najbardziej ambitne twierdzenia prawdopodobnie od razu będą powstawały w duecie: człowiek wymyśla, maszyna weryfikuje, krok po kroku, bez taryfy ulgowej.