Od genialnego samotnika do matematyki jako projektu programistycznego
Przez wieki matematycy polegali wyłącznie na kartce papieru, długopisie i czujnym oku kolegów po fachu. Dziś do gry wchodzi cichy pomocnik działający w tle — program Lean. Coraz więcej czołowych matematyków poddaje swoje najbardziej skomplikowane dowody linijka po linijce weryfikacji przez specjalistyczne oprogramowanie.
Programy takie jak Lean przeczesują tysiące stron wzorów, wyłapują błędy i wydają jednoznaczny werdykt: czy dowód naprawdę się zgadza, czy gdzieś kryje się luka? To fundamentalna zmiana w sposobie uprawiania matematyki.
W klasycznym wyobrażeniu matematyk siedzi samotnie w pokoju otoczony notatnikami. Po miesiącach lub latach pracy gotowy dowód trafia do kolegów, którzy cierpliwie go czytają. Ten model przetrwał trzy tysiące lat — od Archimedesa aż po późny wiek dwudziesty.
Teraz ten obraz wyraźnie się zmienia. Jednym z przełomowych momentów była praca niemieckiego matematyka Petera Scholzego, laureata prestiżowego Medalu Fieldsa. Opublikował on niezwykle techniczną teorię dotyczącą tak zwanych „skroplonych przestrzeni" — zagadnienia, w którym naprawdę biegle orientuje się zaledwie garstka specjalistów na świecie.
Lean jako cyfrowy współczytający
Scholze nie czuł się pewnie. Jego dowód liczył setki stron wypełnionych subtelnymi krokami, które łatwo mogły pójść w złym kierunku. Zamiast kolejny raz prosić kolegów o lekturę, postanowił działać zupełnie inaczej.
W 2020 roku uruchomił Liquid Tensor Experiment — otwarte zaproszenie dla każdego, kto potrafił pracować z Lean, czyli tak zwanym asystentem dowodów. To oprogramowanie przekształca matematyczne rozumowania w formalny kod, a następnie przykłada każdy krok do ścisłej logicznej miarki.
Międzynarodowa grupa badaczy rzuciła się do pracy. Tłumaczyli złożone rozumowanie Scholzego na kod kawałek po kawałku, aż powstało około 180 000 linii. Lean niestrudzenie przechodził przez każdą z nich, sprawdzając, czy każdy krok wynika z poprzednich oraz z przyjętych definicji pojęć.
Tam gdzie ludzka weryfikacja zawsze opiera się częściowo na zaufaniu, Lean bije na alarm dopiero wtedy, gdy wszystko formalnie się zgadza.
Po pół roku intensywnej pracy nadeszła odpowiedź: dowód wytrzymał próbę, bez żadnych logicznych luk. Dla Scholzego oznaczało to pewność, której żaden ludzki recenzent nie mógłby nigdy zagwarantować. Dla całego środowiska był to symboliczny zerwanie z dawną tradycją opartą na zasadzie „wierzcie nam, sprawdzaliśmy długo".
Niemożliwe projekty stają się weryfikowalne
Asystenty dowodów robią coś więcej niż uspokajanie wybitnych matematyków. Sprawiają, że projekty uważane dotąd za praktycznie niewykonalne stają się nagle realne.
Znakomitym przykładem jest praca Maryny Wiazowskiej, która rozwiązała wielowiekowy problem dotyczący najbardziej efektywnego układania kul w ośmiu wymiarach. Jej dowód słynie z elegancji, lecz zawiera również fragmenty matematyki o ekstremalnej gęstości. Ręczna weryfikacja całości wymagałaby wielu lat pracy dużego zespołu specjalistów.
Międzynarodowy zespół postanowił sformalizować dowód w Lean. Przez wiele miesięcy zamieniali formułę po formule w formalne stwierdzenia, które oprogramowanie mogło przetworzyć. Dopiero gdy każdy element istniał jako kod, Lean mógł przejść przez cały gmach rozumowania.
- Każdy krok musiał ściśle opierać się na krokach poprzednich.
- Żadne założenie nie mogło przemknąć się ukradkiem.
- Każda użyta definicja została precyzyjnie zapisana w kodzie.
W 2024 roku pełna wersja dowodu Wiazowskiej w Lean pojawiła się online. Po raz pierwszy istniało formalne potwierdzenie, którego ludzie sami nie byliby w stanie dostarczyć w rozsądnym czasie. Projekt pokazał, że nawet skrajnie skomplikowane wyniki nie muszą już wiecznie pozostawać w szarej strefie niepewności.
Mathlib — rosnąca skrzynka z narzędziami
Ważną przyczyną, dla której takie projekty są dziś wykonalne, jest ogromny rozrost Mathlib — centralnej biblioteki Lean. Zawiera ona już ponad 1,2 miliona linii kodu: definicje, twierdzenia i wcześniej sformalizowane dowody.
Kto chce wprowadzić nowy dowód do Lean, nie musi zaczynać od zera. Większość podstawowych pojęć i standardowych wyników jest już tam zapisana. Oszczędza to pracy i zapobiega wielokrotnemu wynajdowaniu koła.
Każde sformalizowane twierdzenie staje się cegiełką, na której inni mogą natychmiast budować.
Biblioteka rozrasta się na wzór projektu open source: dziesiątki badaczy codziennie dodają mniejsze i większe fragmenty. Razem przesuwają granicę tego, co jest weryfikowalne.
Oprogramowanie wskazuje błędy w nagrodzonych dowodach
Asystenty dowodów nie rozdają wyłącznie zielonych znaczków. Potrafią być boleśnie szczere. W 2021 roku pewien ważny, nagrodzony wynik był formalizowany w Lean. W połowie procesu oprogramowanie odmówiło dalszego działania: jeden z kroków pośrednich okazał się sprzeczny z własnymi założeniami dowodu.
Zaangażowani matematycy musieli doprecyzować swoje rozumowanie. Żaden ludzki recenzent nie zauważył tego szczegółu, choć różni eksperci starannie czytali pracę. Błąd nie unieważniał wyniku, ale doskonale pokazał, jak łatwo subtelna nieścisłość wymyka się przez sito oceny.
Tego rodzaju doświadczenia wywołują mentalną rewolucję. Tam gdzie opublikowany dowód oznaczał dawniej „zaakceptowany do odwołania", rodzi się teraz nowa kategoria: wyniki w pełni sformalizowane i zweryfikowane przez oprogramowanie.
Od niszowego narzędzia do codziennego pomocnika
Przez długi czas asystenty dowodów były zabawkami logików i informatyków. Krzywa uczenia była stroma, interfejs topory, a próg wejścia dla klasycznie wykształconych matematyków — bardzo wysoki. Ten obraz zmienia się szybko.
Nowe wersje Lean i podobnych programów zyskują przyjazne środowiska pracy, w których wspomagają je modele sztucznej inteligencji. Matematycy mogą teraz między innymi:
- wpisać dowód napisany ręcznie i automatycznie otrzymać sugestie formalnego tłumaczenia;
- sprawdzić, których lematów (pomocniczych twierdzeń) brakuje, by dany krok był kompletny;
- na bieżąco widzieć, w którym miejscu rozumowania logika się zatrzymuje.
Wielu doktorantów uczy się dziś obsługi tych narzędzi już w trakcie studiów. Przynoszą tę metodę pracy do projektów badawczych, co przyspiesza jej upowszechnienie.
Jak dokładnie działają te systemy?
Asystenty dowodów takie jak Lean, Coq czy Isabelle działają zupełnie inaczej niż spektakularne systemy generujące teksty lub obrazy. Są za to kompromisowo rygorystyczne. W uproszczeniu proces przebiega w trzech krokach:
| Krok | Co się dzieje? |
|---|---|
| 1. Formalizacja | Matematyk przepisuje dowód w sztywnym, programistycznym języku pozbawionym niejednoznaczności. |
| 2. Rozkład | Dowód zostaje podzielony na bardzo małe, weryfikowalne kroki i twierdzenia pomocnicze. |
| 3. Weryfikacja | Oprogramowanie sprawdza, czy każdy krok wynika logicznie z kroków wcześniejszych i z przyjętych definicji. |
Tam gdzie ludzie rozumują w większych blokach i pomijają szczegóły, oprogramowanie wymusza radykalną precyzję. Kosztuje to czas, ale daje pewność na poziomie niespotykanym dotąd w historii matematyki.
Napięcie między kreatywnością a bezwzględną kontrolą
Wśród matematyków toczy się żywa dyskusja: ile miejsca zostawić formalnej weryfikacji, a ile swobody twórczym skokom? Eleganckie, intuicyjne rozumowanie na tablicy może w kilku linijkach wyjaśnić, o co chodzi, podczas gdy formalna wersja zajmuje dziesiątki stron kodu.
Wielu badaczy dostrzega dlatego rodzący się podział zadań. Intuicji używają do wymyślania nowych pomysłów, szkicowania surowych koncepcji i dostrzegania związków między pozornie odległymi dziedzinami. Dopiero gdy wynik naprawdę waży wiele — na przykład gdy rozwiązuje znane otwarte pytanie — do gry wchodzi oprogramowanie, by sprawdzić, czy wszystkie szczegóły są żelazne.
W praktyce wykształca się hybryda:
- ludzie formułują hipotezy, szkice i twórcze przeskoki myślowe;
- oprogramowanie pomaga porządkować, strukturyzować i weryfikować ostateczną wersję;
- zespoły rozsiane po całym świecie mogą równocześnie pracować nad różnymi częściami tego samego dowodu.
Co to oznacza dla przyszłości matematyki?
Jeśli obecny trend się utrzyma, liczba formalnie zweryfikowanych twierdzeń będzie szybko rosła. Powstanie w ten sposób swoisty „twardy rdzeń" wyników, na których przyszłe pokolenia będą mogły bezpiecznie budować bez obawy, że gdzieś ukrywa się błąd.
Ma to też konsekwencje dla edukacji. Studenci będą mogli ćwiczyć w środowisku, gdzie oprogramowanie natychmiast wskazuje miejsce, w którym ich rozumowanie się sypie. Wykładowcy zyskają lepszy wgląd w to, który krok dowodu sprawia uczniom trudność. A młodzi badacze wcześnie nauczą się, że klarowne formułowanie myśli w formalnym języku to nie żaden szczegół, lecz potężne narzędzie.
Dla postronnych może to brzmieć chłodno — jakby z matematyki znikała romantyka. W rzeczywistości wielu matematyków patrzy na to inaczej. Oddając żmudną pracę kontrolną komputerowi, zyskują więcej przestrzeni na twórcze skoki, odważne pomysły i nieoczekiwane połączenia. Wielkie twierdzenie może sprawdzać Lean, ale pierwsza iskra zawsze rodzi się w głowie człowieka trzymającego ołówek.
