Rewolucja w matematyce: programy komputerowe sprawdzają dziś najtrudniejsze dowody

Do gry wchodzi oprogramowanie, które nie popełnia ludzkich pomyłek.

Przez trzy tysiące lat matematycy opierali się na tym samym rytuale: samotna praca, długa, żmudna weryfikacja przez nieliczne grono ekspertów, nadzieja, że nikt niczego nie przeoczył. Dziś ten porządek pęka. Pojawiają się programy, które śledzą każde działanie w dowodzie niczym bezlitosny korektor, linijka po linijce, aż do ostatniego symbolu.

Od samotnego geniusza do pracy w duecie z maszyną

Jeszcze niedawno wyobrażenie matematyka było proste: samotny naukowiec, zanurzony w notatkach, walczący z abstrakcyjnymi pojęciami. Taki obraz funkcjonował od czasów Archimedesa aż po XXI wiek. Dzisiaj coraz częściej do tego duetu dołącza komputer, a w szczególności tak zwany „asystent dowodowy” – specjalistyczne oprogramowanie weryfikujące poprawność rozumowania.

Symbolem tej zmiany stała się historia Petera Scholzego, jednego z najwybitniejszych matematyków młodego pokolenia. Mimo najwyższych wyróżnień, po opublikowaniu ogromnego, wielusetstronicowego dowodu dotyczącego tzw. przestrzeni skondensowanych, sam przestał być pewny, czy w którymś miejscu nie wkradł się błąd. Problem był zbyt trudny, by kilku recenzentów mogło w rozsądnym czasie sprawdzić każdy szczegół.

Zamiast czekać latami na ostateczną opinię środowiska, Scholze postanowił pójść całkiem inną drogą. Ogłosił międzynarodowy projekt, w którym zaprosił matematyków i informatyków do przepisania jego pracy do języka zrozumiałego dla programu Lean – jednego z najpopularniejszych asystentów dowodowych.

Asystent dowodowy to program, który nie tyle „rozwiązuje” zadania za matematyków, lecz czujnie sprawdza poprawność każdego kroku, nie pozwalając przejść dalej, jeśli gdziekolwiek pojawi się luka w rozumowaniu.

Po zaledwie sześciu miesiącach zespołowej pracy rozrzuconej po całym globie maszyna zakończyła analizę. 180 tysięcy linii formalnego zapisu przeszło przez sito Leana bez żadnego alarmu. Scholze dostał coś, czego zwykła recenzja naukowa nie jest w stanie zagwarantować: niemal absolutną pewność, że dowód trzyma się w każdym, nawet najdrobniejszym detalu.

Matematyka zbiorowa zamiast samotnej wieży z kości słoniowej

Wraz z wejściem takich narzędzi zmienia się także organizacja pracy. Do tej pory ogromne twierdzenia często spoczywały na barkach jednego, dwóch autorów i kilku recenzentów. Teraz jeden projekt może angażować dziesiątki osób, które równolegle zajmują się różnymi fragmentami dowodu, a program czuwa nad spójnością całości.

Lean, Coq czy Isabelle pozwalają podzielić rozumowanie na maleńkie, bardzo precyzyjne kroki. Każdy uczestnik dodaje swój „klocek”, a oprogramowanie natychmiast sprawdza, czy pasuje do reszty konstrukcji. To zupełnie inna dynamika niż wielomiesięczna cicha wymiana maili między pojedynczym autorem a recenzentami.

• autorzy zyskują szybszą i ostrzejszą weryfikację swoich pomysłów,
• młodsi badacze mogą dołączać do projektów, zaczynając od małych, precyzyjnych zadań,
• ryzyko przeoczenia błędu maleje, bo każdą lukę natychmiast „widzi” program.

Problemy „niemożliwe do sprawdzenia” wreszcie pod lupą

Duże twierdzenia z natury są trudne. Niektóre z nich przez dekady wisiały w próżni: społeczność akceptowała ich poprawność, lecz pełna, linijka po linijce weryfikacja była po prostu niewykonalna. Zbyt dużo stron, zbyt gęsta symbolika, zbyt mało ekspertów, którzy byliby w stanie poświęcić na to lata życia.

Dobrym przykładem stała się praca Maryny Wiazowskiej nad upakowaniem kul w ośmiu wymiarach – jednym z klasycznych, ekstremalnie trudnych problemów. Jej dowód zyskał ogólne uznanie; nieliczni specjaliści przeczytali go i nie znaleźli zastrzeżeń. Nie znaczyło to jednak, że ktoś naprawdę prześledził każdy krok jak w podręcznikowym zadaniu.

Dlatego zespół badaczy postanowił przenieść całą tę konstrukcję do Leana. Zadanie zajęło wiele miesięcy i wymagało ścisłej współpracy matematyki „na papierze” z formalnym kodem. Ostatecznie powstał kompletny zapis, który program przyjął bez sprzeciwu. Oznacza to, że raz na zawsze rozpisano dowód w sposób, który nie pozostawia miejsca na niedopowiedzenia czy skróty myślowe.

Kluczowe jest tu jeszcze coś innego: każda sformalizowana praca trafia do wspólnej bazy wiedzy. W wypadku Leana nosi ona nazwę Mathlib i liczy już ponad milion linii definicji oraz twierdzeń. Ktoś, kto zaczyna nowy projekt, nie musi za każdym razem odtwarzać znanych faktów od zera. Może spokojnie odwołać się do gotowych, zweryfikowanych klocków i budować na nich kolejne piętra.

Maszyna wyłapuje błędy, którym ulegli recenzenci

Rozrastające się biblioteki i coraz większe doświadczenie z programami prowadzą też do mniej wygodnych wniosków dla naukowców. Asystenty dowodowe potrafią wskazać błędy w pracach, które wcześniej przeszły przez pełną procedurę recenzyjną i zdobyły nagrody.

W jednym z głośniejszych przypadków zespół matematyków postanowił sformalizować ważne twierdzenie uhonorowane prestiżową nagrodą. Podczas przepisywania argumentacji do Leana program zatrzymał się na jednym z kroków. Po dokładniejszej analizie okazało się, że w dowodzie rzeczywiście brakowało jednego założenia, przez co fragment nie był w pełni uzasadniony. Nikt wcześniej tego nie zauważył, chociaż tekst czytało wielu specjalistów.

Program nie posiada intuicji ani „wyczucia”, za to konsekwentnie wymaga, by każde przejście w rozumowaniu dało się wyjaśnić wprost, w ścisłym języku logiki.

Ta bezkompromisowość budzi respekt, ale też rodzi naturalne obawy: ile innych klasycznych prac zawiera podobne, drobne potknięcia? I jak mocno powinniśmy zmienić nasze zaufanie do publikacji naukowych, kiedy wiemy już, że maszyna potrafi wyłapać rzeczy niewidoczne dla najlepszych recenzentów?

AI pomaga matematykowi pisać „po komputerowemu”

Do niedawna barierą był sam sposób komunikacji z programem. Asystenty dowodowe wymagają bardzo precyzyjnego, często dość sztywnego „języka”, który przypomina programowanie. Wielu matematyków po prostu nie miało czasu ani chęci, aby uczyć się kolejnego złożonego narzędzia na równi z opanowywaniem teorii.

Na tym etapie wkracza nowa fala narzędzi AI. Modele językowe pomagają tłumaczyć zwykłe, matematyczne zapisy – te znane z notatek i artykułów – na formalny kod akceptowany przez Leana czy inne systemy. Badacz opisuje krok rozumowania tak, jak robił to zawsze, a sztuczna inteligencja proponuje jego ścisłą wersję, którą program może już przetworzyć.

Dzięki temu bariera wejścia spada. Z narzędzi zaczynają korzystać osoby, które wcześniej unikały programowania. Proces formalizacji, choć nadal wymagający i czasochłonny, staje się znacznie przyjaźniejszy i bliższy naturalnemu sposobowi pracy matematyka.

Co ta zmiana oznacza dla przyszłości matematyki

Połączenie ludzkiej kreatywności i maszynowej skrupulatności tworzy nowy model pracy. Człowiek wymyśla pomysły, szuka wzorców, zgaduje, gdzie może kryć się rozwiązanie. Komputer wchodzi do gry, gdy trzeba dowieść wszystkiego do końca, bez choćby jednego „oczywiste jest, że…”, którego nie da się rozpisać na równania.

Ta hybryda przynosi kilka ważnych skutków. Po pierwsze, podnosi poprzeczkę dla jakości dowodów – widać coraz wyraźniej różnicę między argumentem intuicyjnym a w pełni rozpisaną konstrukcją formalną. Po drugie, zachęca do projektów, których wcześniej nikt by się nie podjął ze względu na ich skalę. Skoro weryfikacją może zająć się maszyna, łatwiej myśleć o twierdzeniach liczących setki, a nawet tysiące stron matematyki.

Trzeci aspekt dotyczy edukacji. Praca z asystentem dowodowym uczy niesamowitej precyzji. Student, który musi rozpisać argument tak, aby zrozumiał go program, zaczyna lepiej widzieć, gdzie faktycznie używa jakiego założenia, a gdzie tylko polega na intuicji. To może zmienić sposób uczenia matematyki na zaawansowanym poziomie.

W tle pozostaje jeszcze pytanie o granice: czy kiedyś to program sam zacznie proponować nowe twierdzenia, a człowiek stanie się bardziej redaktorem niż autorem? Na razie scenariusz wygląda inaczej – to ludzie napędzają pomysły, a maszyny pomagają je oczyścić z nieścisłości. Coraz więcej wskazuje jednak na to, że bez takiej współpracy kolejne wielkie przełomy byłyby zwyczajnie niewykonalne do rzetelnego sprawdzenia.