Rewolucja w matematyce: komputery zaczynają sprawdzać wielkie twierdzenia

Przez tysiące lat matematycy polegali wyłącznie na kartce, ołówku i wzajemnym zaufaniu.

Teraz do gry wchodzą specjalne programy.

Nowe narzędzia, takie jak system Lean, analizują dowody krok po kroku i wychwytują luki, których ludzkie oko zwyczajnie nie dostrzega. To nie jest drobny dodatek do pracy badacza, ale zmiana sposobu, w jaki powstają i są weryfikowane jedne z najtrudniejszych twierdzeń naszych czasów.

Od samotnego geniusza do zespołu wspieranego przez algorytmy

Przez wieki w matematyce dominował podobny schemat: ktoś wymyśla dowód, opisuje go w długim artykule, a potem garstka ekspertów próbuje go sprawdzić. Taki proces zajmował miesiące, czasem lata, a i tak nigdy nie dawał stuprocentowej pewności, że w gąszczu wzorów nie czai się błąd.

Przykład Petera Scholzego dobrze pokazuje, jaką cenę płacili nawet najlepsi. To jeden z najbardziej znanych współczesnych matematyków, laureat prestiżowej nagrody Fields. Mimo tego, kilka lat temu nie był pewien własnego, ogromnie złożonego twierdzenia dotyczącego tak zwanych przestrzeni skondensowanych. Dowód liczył setki stron, a jego poprawność była poza zasięgiem większości specjalistów.

Zamiast prosić o kolejne tradycyjne recenzje, Scholze postawił na zupełnie inne podejście. Zaproponował projekt nazwany Liquid Tensor Experiment i zaprosił programistów oraz matematyków korzystających z systemu Lean, aby przepisali jego argumenty na język formalny, zrozumiały dla komputera.

Asystent dowodów taki jak Lean nie „wierzy na słowo” nawet największym autorytetom. Każde przejście od jednego kroku do drugiego musi być ściśle uzasadnione według rygorystycznych reguł logiki.

Po około pół roku zespół pracujący nad projektem ogłosił zakończenie zadania. Maszyna przeanalizowała około 180 tysięcy linii formalnego kodu. Żadnej sprzeczności, żadnej luki. Scholze dostał to, czego nie dawał nawet najbardziej życzliwy i kompetentny recenzent: niemal absolutną pewność, że jego rozumowanie trzyma się w całości.

Matematyka w chmurze: wspólna praca nad jednym dowodem

Program Lean okazał się czymś więcej niż tylko automatycznym korektorem. Umożliwił dziesiątkom badaczy z różnych krajów pracę nad jednym, ogromnym dowodem, jednocześnie i w sposób uporządkowany. Każdy uczestnik mógł przejąć wybrany fragment argumentacji, opisać go w postaci formalnej, a program natychmiast sprawdzał zgodność z wcześniejszymi krokami.

Z czasem wokół tego typu narzędzi wyrosły duże, stale rozwijane zbiory twierdzeń. Najsłynniejszy w świecie Leana jest projekt Mathlib – biblioteka zawierająca już ponad milion linii definicji, lematu po lemacie, wszystko sprawdzone komputerowo. To coś w rodzaju matematycznego „systemu operacyjnego”, do którego każdy może dopisać kolejne moduły.

• matematyk proponuje nową ideę lub szkic dowodu,
• zespół tłumaczy ją na formalny język używany przez Lean, Coq czy Isabelle,
• asystent krok po kroku kontroluje logikę,
• po akceptacji fragment trafia do wspólnej biblioteki jako kolejne solidne ogniwo teorii.

Taki model pracy rozbija mit o „samotnym geniuszu” działającym w odcięciu od reszty. Przypomina raczej duży projekt informatyczny rozwijany przez społeczność open source, tyle że w roli kodu pojawiają się wzory i definicje.

Gigantyczne twierdzenia, które wreszcie da się sprawdzić

Kolejny głośny przykład to praca Maryny Viazovskiej nad upakowaniem kul w ośmiu wymiarach. Problem ma długą historię, a rozwiązanie przyniosło badaczce nagrodę Fields. Jej dowód był jednak tak złożony, że pełne ręczne przejście przez każdy szczegół wydawało się praktycznie nierealne.

Grupa matematyków postanowiła przełożyć cały ten argument na język używany przez Lean. Zadanie trwało miesiącami i wymagało ścisłej współpracy osób z różnych ośrodków. Kiedy formalny kod pojawił się na GitHubie, komputer bezlitośnie sprawdził każdy krok. Rezultat: formalne potwierdzenie poprawności twierdzenia, którego żaden pojedynczy człowiek nie byłby w stanie zweryfikować do końca.

Asystenty dowodów zamieniają „za duże, żeby to sprawdzić” w „niewygodne, ale wykonalne”. Dla wielu trudnych problemów to jakościowa zmiana.

W tradycyjnym modelu część dowodów pozostawała w zawieszeniu. Społeczność akceptowała je w oparciu o reputację autorów i ogólną spójność, ale nikt nie miał czasu ani sił, by przepracować każdy mikroskopijny szczegół. Automatyzacja odsuwa tę barierę dalej: pozwala podejść do projektów, które dawniej trafiałyby do szuflady z adnotacją „zbyt wielkie, by je rzetelnie sprawdzić”.

Maszyna wyłapuje błędy, które przechodzą przez recenzje

Systemy typu Lean mają też mniej wygodne oblicze: potrafią wskazać błąd w pracy uznanej już przez środowisko i nagrodzonej prestiżową nagrodą. Tak stało się z jednym z głośnych twierdzeń sformalizowanych w ostatnich latach. W trakcie przepisywania dowodu na język formalny program zatrzymał się na pewnym kroku i zwyczajnie odmówił przyjęcia argumentu.

Okazało się, że w środku rozumowania brakowało kluczowego założenia. Ludzie, nawet bardzo doświadczeni recenzenci, pominęli ten detal. Maszyna nie miała takiej możliwości – musi mieć „zamknięty obieg” logiki od A do Z, inaczej nie ruszy dalej.

Dla wielu badaczy to bolesna lekcja pokory. Z drugiej strony, rośnie zaufanie do twierdzeń, które przeszły przez formalną weryfikację. Odbiorca nie musi polegać wyłącznie na autorytecie nazwiska. Ma do dyspozycji pełny, maszynowo sprawdzony zapis, w którym każde ominięcie skrótu myślowego natychmiast kończy się komunikatem o błędzie.

Jak działa asystent dowodów taki jak Lean

Warto rozłożyć to na prostsze elementy. Programy tego typu działają w kilku krokach:

Od strony użytkownika przypomina to pracę z bardzo wymagającym kompilatorem. Nie wystarczy pomysł ani ogólna struktura. Każde przejście między wzorami musi zostać udokumentowane w sposób, który rozumie precyzyjna maszyna.

Sztuczna inteligencja ułatwia wejście do gry

Przez lata barierą w korzystaniu z takich narzędzi była sama technika. Trzeba było znać składnię systemu, myśleć jak programista, a nie każdy matematyk ma do tego cierpliwość. Teraz zaczyna się to zmieniać dzięki AI.

Modele językowe, podobne do tych napędzających ChatGPT, potrafią pomagać w tłumaczeniu tradycyjnego dowodu na kod formalny. Użytkownik podaje szkic w zwykłym języku matematycznym, a asystent AI podpowiada, jak zapisać to w notacji Lean. W ten sposób bariera wejścia stopniowo maleje i coraz więcej badaczy, którzy nigdy nie programowali zawodowo, zaczyna korzystać z automatycznej weryfikacji.

Współpraca nie polega na tym, że maszyna „wymyśla matematykę za ludzi”. Człowiek dostarcza intuicję i pomysły, komputer pilnuje logicznej szczelności całej konstrukcji.

Co to oznacza dla przyszłych pokoleń matematyków

Dla młodych badaczy nowa sytuacja ma dwie strony. Z jednej muszą nauczyć się dodatkowego języka – nie tylko analizy, algebry czy topologii, ale też obsługi narzędzi formalnych. Z drugiej dostają potężne wsparcie: mogą budować kariery na projektach, które jeszcze dekadę temu były poza technicznym zasięgiem pojedynczych osób.

Zmienia się też nauczanie. Kursy z użyciem Leana czy Coq stają się coraz popularniejsze na uniwersytetach. Student nie tylko „wierzy na słowo”, że pewien dowód jest poprawny, ale może zobaczyć, jak przechodzi przez sito programu. To zupełnie inne doświadczenie niż tylko przepisywanie wzorów z tablicy.

Ryzyka, nadzieje i praktyczne skutki

Nowe podejście nie jest wolne od obaw. Część środowiska martwi się, że zbyt silne oparcie na narzędziach informatycznych może zepchnąć na drugi plan piękno i prostotę tradycyjnych dowodów. Istnieje też ryzyko, że społeczność podzieli się na tych, którzy „potrafią w Lean”, i tych, którzy zostaną na marginesie.

Z drugiej strony rośnie szansa na zmniejszenie liczby głośnych wpadek naukowych. Publikacje oparte na formalnej weryfikacji stoją na znacznie stabilniejszym gruncie. Dla zastosowań praktycznych – w kryptografii, teorii kodowania, finansach ilościowych – to ma bardzo wymierne znaczenie. Błąd w twierdzeniu matematycznym użytym w protokole bezpieczeństwa może kosztować miliardy; narzędzia automatycznej kontroli zmniejszają takie ryzyko.

Najciekawsze jest to, że narzędzia te nie są zarezerwowane wyłącznie dla wąskiej elity. Każdy, kto ma odpowiednią wiedzę i odrobinę cierpliwości, może dziś pobrać Leana, przejrzeć Mathlib i spróbować samodzielnie sformalizować ulubione twierdzenie z analizy czy geometrii. Dla części osób stanie się to naturalnym rozszerzeniem klasycznego warsztatu, podobnie jak kiedyś kalkulator czy komputer algebraiczny.

Coraz wyraźniej widać więc, że matematyka nie traci na tej zmianie swojej głębi ani „duszy”. Zyskuje za to nowego partnera – wymagającego, bezlitosnego w punkcie, ale niezwykle pomocnego w utrzymaniu całości na logicznym fundamencie. A to otwiera drogę do twierdzeń tak rozległych, że jeszcze niedawno nikt nie ośmielał się ich w pełni sprawdzić.