Komputery sprawdzają dziś twierdzenia matematyczne lepiej niż ludzie

Coraz więcej matematyków oddaje swoje najtrudniejsze twierdzenia w ręce specjalnych programów, które analizują dowody linijka po linijce.

To, co przez tysiące lat było samotną pracą z kartką i ołówkiem, zmienia się w zespołowe projekty z udziałem oprogramowania Lean, Coq czy Isabelle. Maszyny nie wymyślają jeszcze nowych teorii, ale stają się bezwzględnymi kontrolerami, które nie przepuszczą żadnej nielogicznej linii rozumowania.

Od kartek i ołówka do kodu: wielka zmiana w matematyce

Przez wieki schemat wyglądał tak samo. Badacz wymyślał dowód, pisał go w formie artykułu, a potem grupa recenzentów przez miesiące, czasem lata, sprawdzała, czy wszystkie kroki są poprawne. Im bardziej skomplikowany problem, tym większe ryzyko, że coś umknie nawet najlepszym ekspertom.

Dziś do gry wchodzą tzw. asystenci dowodów – programy komputerowe, które formalizują i sprawdzają twierdzenia w specjalnym języku. Każda definicja, każde przejście od kroku A do kroku B musi zostać zapisane precyzyjnie, tak aby komputer mógł ocenić, czy jest zgodne z logiką i wcześniejszymi założeniami.

Matematyk wciąż wymyśla pomysł na dowód, ale to program bezlitośnie weryfikuje każdy szczegół, odrzucając najmniejszą nieścisłość.

Tego rodzaju narzędzia istniały już wcześniej, lecz dopiero ostatnie lata przyniosły ich prawdziwy przełom – zarówno pod względem możliwości, jak i liczby badaczy, którzy faktycznie zaczęli z nich korzystać w poważnych projektach.

Gdy geniusz sam sobie nie ufa: przypadek Petera Scholzego

Dobrym symbolem tej zmiany jest historia Petera Scholzego, jednego z najbardziej znanych współczesnych matematyków, laureata medalu Fieldsa. W 2018 roku opublikował on ogromny, niezwykle abstrakcyjny dowód dotyczący tzw. przestrzeni skondensowanych. Materiał liczył setki stron i dotyczył obszaru tak technicznego, że na świecie istniało zaledwie kilka osób, które w ogóle mogły go przeczytać ze zrozumieniem.

Scholze wcale nie był spokojny. Miał świadomość, że przy takiej skali szczegółów łatwo o błąd ukryty w jednym z licznych pośrednich kroków. Zamiast prosić kolejnych kolegów o heroiczne wielomiesięczne recenzje, poszedł w inną stronę.

Liquid Tensor Experiment: globalny projekt na kodzie

W 2020 roku ruszył projekt znany jako Liquid Tensor Experiment. Scholze zaprosił matematyków i programistów z całego świata do przepisania jego dowodu na język programu Lean. Celem było nie tylko „przeklepanie” formuł, ale pełna formalizacja, którą Lean jest w stanie mechanicznie zweryfikować.

Efekt? Po około pół roku pracy międzynarodowy zespół zakończył projekt. Powstało aż około 180 tysięcy linii kodu opisujących szczegóły dowodu. Program nie znalazł żadnej sprzeczności, żadnego nieuzasadnionego przeskoku. Scholze otrzymał więc coś, czego wcześniej matematycy praktycznie nie mieli: formalną, komputerową gwarancję poprawności swojej pracy.

Takie projekty zmieniają obraz zawodu matematyka – z samotnej pracy przy biurku na skoordynowane działania wielu osób, które współdzielą jeden ogromny kod dowodu.

Przy okazji okazało się, że narzędzie, które początkowo wydawało się przeznaczone dla garstki entuzjastów logiki i informatyki, może realnie wejść do mainstreamu współczesnych badań.

Dowody, których nikt nie odważyłby się ręcznie przejrzeć

Asystenci dowodów najlepiej pokazują swoją siłę tam, gdzie ludzkie możliwości po prostu się kończą. Świetnym przykładem jest praca Maryny Viazovskiej nad problemem upakowania sfer w przestrzeni o wymiarze 8. To zagadnienie miało długą historię, a jej rozwiązanie przyniosło jej medal Fieldsa w 2022 roku.

Dowód Viazovskiej był niezwykle gęsty, pełen wyrafinowanych konstrukcji analitycznych. Teoretycznie niezależna kontrola każdego szczegółu przez zespół ekspertów była możliwa, ale zajęłaby im całe lata i pochłonęłaby ogromne zasoby. W praktyce nikt nie miałby na to czasu ani siły.

Lean jako bezlitosny recenzent

Grupa matematyków postanowiła więc przenieść jej argumentację do Lean. Przez wiele miesięcy krok po kroku budowali formalną wersję dowodu. Program wymagał dokładnej deklaracji wszystkich hipotez, pojęć pośrednich i zależności. Tam, gdzie w tradycyjnym artykule autor pisze „z tego wynika to”, w Lean trzeba precyzyjnie pokazać, na jakich wcześniejszych twierdzeniach i definicjach opiera się dane przejście.

W 2024 roku na GitHubie opublikowano kompletny kod opisujący ten projekt. Każdy, kto zna Lean, może zobaczyć, jak maszyna przeszła przez cały tok rozumowania i nie zgłosiła sprzeczności. Tym samym jeden z najbardziej imponujących współczesnych wyników matematycznych zyskał niezwykle mocne wsparcie: nie tylko autorytet medalu Fieldsa, lecz także mechaniczne potwierdzenie przez program.

Duże, skomplikowane twierdzenia, które kiedyś wisiały w zawieszeniu, bo nikt nie miał siły ich sprawdzić w całości, teraz mogą dostać komputerowy stempel jakości.

Z takim podejściem łączy się też rozbudowa wspólnej bazy wiedzy. W przypadku Lean kluczową rolę odgrywa biblioteka Mathlib. Zawiera ona już ponad milion linii formalnych definicji i twierdzeń – od podstaw algebry aż po bardzo wyspecjalizowane konstrukcje. Każdy nowy projekt dokłada do tej bazy kolejne cegiełki, co przyspiesza pracę przy następnych zadaniach.

Błędy w nagradzanych twierdzeniach wychwycone przez program

Komputerowe narzędzia nie tylko potwierdzają poprawność udanych dowodów. Potrafią też wskazać miejsca, w których coś się nie zgadza, nawet jeśli tekst przeszedł już przez sito prestiżowych recenzji. Zdarzył się przypadek, w którym zespół matematyków formalizował w Lean twierdzenie uhonorowane ważną nagrodą. W trakcie przepisywania do kodu program zatrzymał się na pozornie niewinnym kroku pośrednim.

Lean pokazał, że jedna z implikacji nie wynika logicznie z wcześniejszych założeń. Autorzy musieli uzupełnić rozumowanie i wprowadzić poprawki. Żaden recenzent nie wychwycił tego wcześniej, choć tekst był już akceptowany przez środowisko. Dopiero wymóg całkowitej formalizacji zmusił badaczy do uporządkowania wszystkich luk i skrótów myślowych.

• Asystent dowodów nie „ufa” autorytetom – liczy się tylko logika.
• Każdy krok musi wynikać z wcześniejszych dokładnie tak, jak opisano.
• Nawet drobna luka uniemożliwia przejście dalej, dopóki nie zostanie naprawiona.

Taka bezkompromisowa postawa programu bywa frustrująca, ale jednocześnie zwiększa zaufanie do zweryfikowanych w ten sposób wyników. Jeśli dowód przeszedł przez wiele tysięcy linii kodu i żaden moduł weryfikujący się nie zbuntował, prawdopodobieństwo ukrytej pomyłki gwałtownie spada.

Jak AI ułatwia życie „zwykłym” matematykom

Jeszcze niedawno narzędzia typu Lean uchodziły za domenę specjalistów od logiki i teoretycznej informatyki. W praktyce wielu matematyków bało się ich, bo kojarzyły się z koniecznością nauki nowego, dość surowego języka programowania. Sytuacja szybko się zmienia, bo do gry wchodzi sztuczna inteligencja.

Pojawiają się interfejsy, które pomagają w tłumaczeniu ręcznie zapisanych argumentów na kod formalny. Modele językowe podpowiadają składnię, uzupełniają oczywiste kroki, a nawet sugerują, które twierdzenia z biblioteki Mathlib warto użyć w danym miejscu. Matematycy nie muszą już wszystkiego wklepywać od zera i poznawać każdego technicznego szczegółu.

W efekcie rośnie grupa badaczy, którzy traktują Lean czy Coq nie jako ciekawostkę, ale jako regularny element pracy. Zaczynają od krótszych wyników, budują własny fragment biblioteki, a potem przechodzą do większych projektów zespołowych.

Co to oznacza dla przyszłości badań matematycznych

Zmiana ma kilka ważnych konsekwencji. Po pierwsze, rośnie skala projektów, które w ogóle można brać na warsztat. Skoro istnieje szansa na mechaniczne sprawdzenie gigantycznych dowodów, badacze odważniej formułują bardzo mocne, techniczne twierdzenia. Wiedzą, że nie będą skazani tylko na ludzką pamięć i uwagę.

Po drugie, rośnie znaczenie pracy zespołowej. Duże formalizacje wymagają współpracy kilkunastu czy kilkudziesięciu osób, które dzielą się zadaniami i wykorzystują wspólną bibliotekę kodu. Matematyka przypomina tu coraz mocniej rozwój dużych projektów open source

Po trzecie, zmienia się sama definicja „dowodu”. Przez długi czas wystarczał artykuł, który przekonywał ekspertów. Teraz coraz częściej mówi się o dwóch etapach: wersji intuicyjnej, przeznaczonej dla ludzi, oraz formalnej, którą może sprawdzić program. W niektórych dziedzinach pełna akceptacja ważnych wyników będzie w przyszłości wymagała właśnie tej drugiej warstwy.

Dla studentów i młodszych badaczy formalne systemy weryfikacji mogą stać się narzędziem edukacyjnym. Zmuszają do precyzji, której zwykle nie wymaga się na wczesnych etapach nauki. Jeśli komputer sygnalizuje błąd, trzeba wrócić do definicji i naprawdę zrozumieć, co ona oznacza, zamiast polegać na ogólnym wrażeniu „to chyba działa”.

Oprogramowanie nie zastępuje więc kreatywności, ale ustawia bardzo wysoki próg dla błędów logicznych. W erze coraz bardziej złożonych teorii taki partner może decydować o tym, czy ambitne projekty pozostaną jedynie szkicami w notatnikach, czy naprawdę staną się w pełni zweryfikowaną częścią matematyki.