Komputery sprawdzają dziś twierdzenia szybciej niż armia matematyków

Coraz więcej matematyków oddaje swoje najbardziej skomplikowane twierdzenia w ręce wyspecjalizowanych programów, które sprawdzają dowody linijka po linijce.

To cicha rewolucja w dziedzinie, która przez tysiące lat opierała się na kartce papieru, ołówku i cierpliwości recenzentów. Teraz do gry wchodzą narzędzia takie jak Lean, Coq czy Isabelle, zamieniając ludzką intuicję w precyzyjny kod, który komputer może bezlitośnie, ale i niezawodnie zweryfikować.

Od samotnego geniusza do pracy w trybie open source

Przez większość historii matematyki schemat był prosty. Jedna osoba lub niewielki zespół opracowywał dowód, publikował go, a reszta środowiska – czasem przez lata – próbowała sprawdzić, czy wszystko się zgadza. W przypadku bardzo technicznych, wielusetstronicowych prac ten proces bywał w praktyce nierealny.

Symbolem zmiany stał się przypadek Petera Scholzego, jednego z najgłośniejszych współczesnych matematyków, laureata medalu Fieldsa. W 2018 roku opublikował on niezwykle złożone twierdzenie dotyczące tzw. przestrzeni kondensowanych. Sam przyznawał, że ma w sobie niepokój: w setkach stron szczegółowych argumentów mogła czaić się drobna, ale brzemienna w skutki pomyłka.

Zamiast prosić kolejne osoby o ręczne sprawdzenie pracy, Scholze postanowił pójść w inną stronę. Uruchomił projekt Liquid Tensor Experiment i zaprosił matematyków oraz informatyków z całego świata, aby przepisali jego dowód do języka używanego przez program Lean, czyli tzw. asystenta dowodzenia.

Asystent dowodzenia to specjalistyczny program, który przyjmuje matematyczne twierdzenia zapisane w formalnym języku i sprawdza każde przejście w rozumowaniu według ściśle zdefiniowanych reguł logiki.

W ciągu sześciu miesięcy międzynarodowy zespół stworzył około 180 tysięcy linii kodu opisujących dowód Scholzego w sposób całkowicie formalny. Komputer przeszedł po nim krok po kroku. Ani jedna logiczna luka nie przeszła przez sito. Niemiecki matematyk zyskał rodzaj pewności, której tradycyjna recenzja naukowa tak naprawdę nigdy nie dawała.

Jak program typu Lean „rozumie” matematykę

Lean, podobnie jak inne asystenty dowodzenia, nie jest magiczną „maszynką do twierdzeń”. Nie wymyśla nowych idei za badaczy. Wymusza za to, by wszystko, co oni twierdzą, dało się zapisać w postaci ciągu bardzo elementarnych kroków, niewymagających żadnej domyślności.

• Matematyk zapisuje definicje, założenia oraz twierdzenia w sformalizowanym języku.
• Rozbija dowód na drobne etapy, często znacznie mniejsze niż w publikacji naukowej.
• Lean śledzi każdy krok i sprawdza, czy wynika on logicznie z poprzednich.
• Jeżeli gdziekolwiek pojawi się luka, sprzeczność lub błąd w typach obiektów, program od razu zgłasza problem.

Żaden recenzent nie ma cierpliwości ani mocy przerobowej, by w takim tempie i z takim poziomem pedanterii przeanalizować wielusetstronicowy dowód. Komputer – owszem.

Ogromne, wcześniej nieweryfikowalne dowody stają się wykonalne

Zmiana nie dotyczy tylko pojedynczych gwiazd matematyki. Coraz częściej całe zespoły biorą na warsztat wybitne i bardzo skomplikowane prace, których ręczne sprawdzenie byłoby męczącym biegiem bez mety.

Przykład: słynne rozwiązanie problemu upakowania kul w ośmiu wymiarach, przedstawione przez Marynę Viazovską. Jej przełomowy wynik został szybko uznany przez środowisko, a sama badaczka otrzymała medal Fieldsa. Mimo to wiele fragmentów dowodu było skrajnie technicznych i zagęszczonych, co utrudniało pełną weryfikację każdej drobnej nierówności czy konstrukcji.

Grupa matematyków zdecydowała się więc przepisać całość do Lean. Praca trwała miesiącami, wymagała rozbicia dużych bloków argumentacji na niezliczone małe kroki, ale w końcu powstał kompletny kod. Maszyna przeszła po nim od początku do końca, potwierdzając spójność rozumowania Viazovskiej.

To typ projektu, którego nikt przy zdrowych zmysłach nie podjąłby się w całości tradycyjnymi metodami – byłby po prostu zbyt długi i zbyt drobiazgowy dla ludzkiego recenzenta.

Z podobnych powodów szybko rośnie znaczenie biblioteki Mathlib, czyli ogromnej bazy definicji i twierdzeń napisanych specjalnie dla Lean. Zawiera już ponad milion linii kodu. Każdy nowy formalny dowód może opierać się na tym fundamencie, zamiast zaczynać od pustej kartki. Przypomina to trochę rozwój oprogramowania open source: kolejne zespoły budują na sprawdzonych modułach innych.

Gdy komputer łapie błąd nagrodzonego twierdzenia

Asystenty dowodzenia zaczynają pełnić jeszcze jedną, bardzo niewygodną, ale cenną rolę: bezkompromisowego kontrolera jakości. Pojawiły się już sytuacje, w których formalizacja znanego, wyróżnionego nagrodą twierdzenia ujawniła lukę, której nikt wcześniej nie zauważył.

Podczas przepisywania jednej z takich prac do Lean program zatrzymał się na pewnym kroku pośrednim. Według ludzkich recenzentów wszystko było w porządku. Dla maszyny brakowało jednak kluczowej części argumentu. Autorzy musieli wrócić do tablicy, dopisać brakujący fragment i dopiero wtedy cały dowód „przeszedł” przez komputer bez błędów.

Z ludzkiej perspektywy to niewielka poprawka. Z punktu widzenia standardów ścisłej logiki – ogromna różnica. Raz sformalizowany dowód staje się w zasadzie niepodważalny, przynajmniej w ramach przyjętego systemu aksjomatów i reguł.

Co ta rewolucja oznacza dla pracy matematyków

Zmienia się codzienny warsztat badaczy. Jeszcze niedawno narzędzia typu Lean wymagały solidnego przygotowania informatycznego. Teraz coraz częściej mają one przyjazne środowiska pracy, a generatywna AI pomaga tłumaczyć „zwykłe” szkice z notesu na formalny kod.

Dla młodych matematyków oznacza to nową kompetencję: obok umiejętności abstrakcyjnego myślenia pojawia się biegłość w opisywaniu tych idei w języku zrozumiałym dla programu. Dla profesorów – możliwość prowadzenia projektów, w których studenci uczą się zarówno nowoczesnej teorii, jak i pracy z narzędziami programistycznymi.

Ryzyka, ograniczenia i bardzo ludzkie obawy

Nie wszyscy patrzą na tę zmianę bezkrytycznie. Pojawiają się pytania, czy nadmierne poleganie na programach nie zniechęci części badaczy do samodzielnego, „ręcznego” mierzenia się z trudnymi miejscami w dowodach. Innych niepokoi ryzyko, że błąd w samym oprogramowaniu mógłby przełożyć się na całe ciągi rzekomo „pewnych” twierdzeń.

Specjaliści odpowiadają, że asystenci dowodzenia też podlegają kontroli. Najważniejsze komponenty tych systemów mają niezwykle małe jądro zaufanego kodu, które programiści i logicy analizują z obsesyjną dokładnością. Co więcej, sporne wyniki można w razie wątpliwości formalizować równolegle w kilku różnych systemach.

Jest też pytanie o charakter samej kreatywności. Maszyna świetnie sprawdza, czy łańcuch rozumowań jest poprawny, ale nie podpowie, skąd ten łańcuch wziąć. Pomysł na dowód, nieoczywiste przeformułowanie problemu, znalezienie zaskakującej analogii między odległymi działami matematyki – to wciąż domena ludzi.

Maszyna nie zabiera matematykom roli wynalazców idei. Przejmuje rolę bezlitosnego korektora, który dba, by żaden błąd nie prześlizgnął się bokiem.

Co z tego będzie miał zwykły użytkownik technologii

Choć twierdzenia o przestrzeniach kondensowanych czy upakowaniach kul brzmią abstrakcyjnie, efekt domina może dotknąć bardzo przyziemnych obszarów. Metody rozwijane dziś przy formalizowaniu czystej matematyki trafiają też do weryfikacji oprogramowania, protokołów kryptograficznych, a nawet projektów układów scalonych.

To oznacza większą szansę, że algorytm szyfrujący nasze dane naprawdę robi to, co obiecują specyfikacje, a kontroler w samolocie czy samochodzie elektrycznym zachowa się zgodnie z projektem w każdej sytuacji granicznej. Dokładnie ta sama logika, która broni się w dowodzie twierdzenia, może bronić nas przed krytycznym błędem w kodzie.

Matematyka, kojarzona z samotnym profesorem pochylonym nad notesem, powoli zamienia się w ogromny, wspólny projekt typu open source, gdzie ludzkie pomysły splatają się z bezlitosną dokładnością maszyn. A to dopiero początek – im większa będzie baza sformalizowanych wyników, tym śmielszych problemów matematycy odważą się dziś dotykać, wiedząc, że w tle czuwa program gotowy sprawdzić każdy, nawet najbardziej karkołomny krok.