Komputer sprawdza dowody lepiej niż geniusze? Cicha rewolucja w matematyce

Od tysięcy lat matematycy polegali na kartce i ołówku. Teraz coraz częściej oddają swoje najtrudniejsze twierdzenia pod lupę programów komputerowych.

Specjalne systemy, takie jak Lean, Coq czy Isabelle, potrafią kontrolować każdy krok rozumowania matematycznego z dokładnością, której człowiek zwyczajnie nie jest w stanie utrzymać przez setki stron. Dla wielu badaczy to nie ciekawostka, ale konieczność: bez pomocy maszyn nie mieliby stuprocentowej pewności, że ich wielkie wyniki naprawdę są poprawne.

Od samotnego geniusza do zespołu z komputerem w tle

Przez wieki matematyka miała dość romantyczny obraz: wybitny umysł, cisza gabinetu, samotna walka z problemem. Kiedy pojawiał się przełom, autor wysyłał tekst do czasopisma, a grupa recenzentów sprawdzała go fragment po fragmencie. To mogło trwać miesiącami, a przy bardzo złożonych dowodach – nawet latami.

Ta procedura ma poważną słabość: człowiek się męczy, gubi w dżungli technicznych szczegółów, czasem ufa reputacji autora i nie dopytuje o każdy drobiazg. Historia matematyki zna wiele przypadków, gdy błąd znajdował się w literaturze przez dekady, bo nikt nie zdołał albo nie odważył się przeanalizować wszystkiego od zera.

Przeczytaj również: Te dwa znaki zodiaku w marcu wraca do nich nierozwiązana sprawa

Gdy nawet laureat medalu Fields zaczyna się wahać

Dobrym przykładem jest historia Petera Scholzego, jednego z najgłośniejszych współczesnych matematyków. Kilka lat po otrzymaniu medalu Fields przedstawił monumentalny wynik dotyczący tak zwanych przestrzeni skondensowanych. Mówimy o teorii tak abstrakcyjnej, że na świecie istnieje tylko garstka specjalistów, którzy naprawdę rozumieją szczegóły.

Dowód liczył setki stron. Scholze nie był pewien, czy w tym gąszczu nie czai się subtelny błąd. Zamiast prosić kolegów o kolejne lata żmudnego czytania, zaproponował coś zupełnie nowego: otwarty projekt, w którym chętni matematycy mieli przepisać jego rozumowanie do języka programu Lean.

Przeczytaj również: Blue Origin chce chronić Ziemię przed asteroidami. Nowa misja NEO Hunter

Tak narodził się tak zwany Liquid Tensor Experiment. Uczestnicy, rozsiani po całym globie, dzielili dowód na małe fragmenty i formalizowali go linijka po linijce, tak aby komputer mógł automatycznie ocenić, czy każdy krok jest poprawny logicznie.

Efekt: około 180 tysięcy linii kodu, przejrzanych z żelazną konsekwencją przez maszynę. Ani jednej luki logicznej, ani jednego “skoku wiary”.

Scholze otrzymał potwierdzenie, jakiego nie dałby mu żaden, nawet najbardziej życzliwy recenzent. Jednocześnie środowisko matematyczne zobaczyło, że takie projekty potrafią łączyć dziesiątki osób i zamieniać z pozoru nieweryfikowalne giganta w zadanie, które można ogarnąć zespołowo.

Przeczytaj również: Naukowcy „wskrzeszają” płytę CD: tysiąc razy więcej danych na krążku

Asystenci dowodu zmieniają zakres tego, co w ogóle da się sprawdzić

Kolejna głośna historia dotyczy Maryny Viazovskiej. W 2016 roku rozwiązała problem upakowania kul w ośmiowymiarnej przestrzeni – zagadnienie dręczące matematyków od stuleci. Jej dowód przyniósł jej później medal Fields i ogromny prestiż.

Problem w tym, że część argumentów była ekstremalnie gęsta technicznie. Gdyby kilkunastu specjalistów próbowało samodzielnie sprawdzić każdy szczegół, mówilibyśmy o latach pracy, a i tak nikt nie miałby stuprocentowej pewności, że niczego nie przeoczono.

Grupa badaczy postanowiła więc przeprowadzić formalizację dowodu w Lean. Projekt wymagał sporo czasu i zaangażowania, ale udało się doprowadzić go do końca. Wszystkie kluczowe elementy rozumowania Viazovskiej zostały zapisane w postaci kodu, który program mógł przeanalizować mechanicznie.

Dopiero po przejściu przez gęstą sieć komputerowych kontroli można było z pełnym spokojem stwierdzić: w tej konstrukcji nie brakuje żadnego mostka, żadnej ukrytej deski.

Gdy “za duże, by sprawdzić” przestaje być wymówką

Takich przykładów przybywa. Jeszcze niedawno wiele bardzo długich lub technicznych dowodów krążyło w obiegu naukowym z wielkim, niewypowiedzianym “prawdopodobnie poprawne” nad głową. Po prostu nikt nie był w stanie w normalnym tempie oraz za rozsądne pieniądze prześwietlić wszystkiego drobiazgowo.

Teraz coraz częściej stosuje się podejście: dzielimy dowód na małe cegiełki, rozdajemy je zespołowi i formalizujemy w systemie typu Lean, Coq albo Isabelle. Każda cegiełka przechodzi przez komputerową kontrolę. Dopiero na końcu składamy całość w spójny budynek.

Żeby to było w ogóle możliwe, powstają wielkie biblioteki gotowych definicji i twierdzeń. W przypadku Lean taką rolę pełni Mathlib. Zawiera już ponad milion linii sformalizowanej matematyki – od prostych faktów znanych z liceum po bardzo wyspecjalizowane wyniki badawcze.

• ogólne struktury algebraiczne, analityczne i topologiczne,
• klasyczne twierdzenia z wielu działów matematyki,
• narzędzia do pracy z liczbami rzeczywistymi i zespolonymi,
• gotowe definicje pojęć z teorii liczb, geometrii czy logiki.

Dzięki temu każdy nowy projekt nie startuje od zera. Badacze korzystają z gotowej infrastruktury i mogą skupić się na własnym problemie. Efekt przypomina rozwój open source w informatyce: ogromne repozytorium wspólnej wiedzy, które przyspiesza wszelkie kolejne prace.

Maszyna łapie błędy, których nie zauważyło żadne ludzkie oko

Asystenci dowodu nie są grzecznymi sekretarzami, którzy grzecznie przepisują rozumowanie. Ich zadanie polega na sprawdzeniu, czy z przyjętych założeń naprawdę wynika to, co autor twierdzi. Bez zaufania, bez skrótów, bez zasłaniania się autorytetem nazwiska na okładce.

Zdarzyło się już, że podczas formalizacji znanego, nagradzanego twierdzenia komputer wskazał krok, który logicznie nie przechodził. Autorzy musieli uzupełnić lukę i poprawić publikację. Żaden z recenzentów nie wychwycił tej nieścisłości – maszyna zrobiła to w kilka sekund po otrzymaniu właściwej reprezentacji problemu.

Dla środowiska był to zimny prysznic: skoro błąd przetrwał recenzje, granty i nagrody, to ile podobnych “drobiazgów” wciąż ukrywa się w literaturze?

Różnica wynika z samej natury pracy. Recenzent musi połączyć w głowie intuicję, skróty myślowe i doświadczenie. Program ma o wiele prostsze zadanie: dostał reguły logiki i szczegółową definicję wszystkiego, na czym pracuje. Jeśli jakiś krok się nie zgadza, po prostu nie przejdzie dalej.

Nowe narzędzia, nowa rola dla sztucznej inteligencji

Jeszcze niedawno obsługa takich systemów wymagała mocnego przygotowania informatycznego. Dziś, dzięki prostszym interfejsom i wsparciu modeli językowych, wielu “zwykłych” matematyków zaczyna używać Lean czy Coq na co dzień.

Sztuczna inteligencja potrafi na przykład zaproponować szkic kodu na podstawie tradycyjnie zapisanej części dowodu. Człowiek poprawia szczegóły, dodaje brakujące kroki, a następnie uruchamia sprawdzanie formalne. W efekcie proces przypomina współpracę z bardzo wymagającym, ale cierpliwym asystentem.

W efekcie rośnie grupa badaczy, którzy potrafią pracować w trybie hybrydowym: część notatek prowadzą tradycyjnie, inne od razu zapisują w języku asystenta dowodu. Taki styl pracy może za kilka lat stać się standardem w wielu dziedzinach badań teoretycznych.

Co to wszystko znaczy dla matematyki i dla nas

Dla samej dyscypliny stawka jest wysoka. Wraz z rozwojem formalnych bibliotek część klasycznej wiedzy zyska drugie życie – tym razem w postaci kodu, który komputer zweryfikował krok po kroku. Tam, gdzie kiedyś opierano się na autorytecie podręcznika, za jakiś czas może stać już bezdyskusyjnie potwierdzony fakt logiczny.

Zmienia się też profil umiejętności, których potrzebuje młody matematyk. Przydaje się nie tylko talent do abstrakcyjnego myślenia, ale też cierpliwość do precyzyjnego zapisu i odrobina “programistycznego” podejścia. W zamian dostaje narzędzia, które pozwalają mu porywać się na problemy jeszcze niedawno uznawane za zbyt skomplikowane, by je rzetelnie sprawdzić.

Dla reszty społeczeństwa ta zmiana ma bardzo praktyczny wymiar. Wiele dziedzin – od kryptografii po inżynierię oprogramowania – opiera się na matematycznych dowodach. Jeśli te dowody przejdą przez sito systemów formalnych, rośnie zaufanie do technologii, z których korzystamy na co dzień: zabezpieczeń bankowości elektronicznej, protokołów komunikacyjnych, algorytmów sterujących infrastrukturą.

Warto też zauważyć, że matematyka staje się przez to bardziej otwarta. Duże projekty formalizacji przypominają wspólne repozytoria kodu: każdy może dołączyć, dodać swój fragment, nauczyć się czegoś od innych. Z perspektywy młodych ludzi, którzy zaczynają przygodę z tematami czysto teoretycznymi, to często bardziej namacalne i motywujące niż czytanie starych monografii w samotności.

Ten zwrot w stronę pracy z komputerem nie odbiera matematyce ludzkiego wymiaru. Intuicja, kreatywne skojarzenia, nieoczekiwane skróty myślowe – to wciąż domena ludzi. Programy pełnią rolę bezlitosnego kontrolera jakości, który doprowadza konsekwencje naszych pomysłów do samego końca. Im bardziej złożone stają się współczesne teorie, tym wyraźniej widać, że bez takiej asekuracji nawet najwybitniejsze umysły zaczynają czuć się niepewnie.