Matematycy oddają swoje dowody w ręce komputerów. Rewolucja na uczelniach

Coraz więcej matematyków nie ufa już wyłącznie kartce i ołówkowi.

Do gry wchodzą programy, które sprawdzają każdy krok ich dowodów.

Od czasów Archimedesa praca matematyka wyglądała podobnie: samotna walka z abstrakcyjnym problemem, a potem długie miesiące oczekiwania, aż inni eksperci sprawdzą szczegóły. Teraz ten rytuał się rwie. Pojawiły się komputerowe „asystenty dowodów”, takie jak Lean, Coq czy Isabelle, które śledzą tok rozumowania linijka po linijce i bezlitośnie wychwytują każdy błąd.

Od samotnego geniusza do zespołu złożonego z ludzi i maszyn

Matematyka długo kojarzyła się z wizją samotnego geniusza, który w ciszy biura lub biblioteki buduje potężne teorie. Przykład Petera Scholzego pokazuje, że ten obraz zaczyna się starzeć. Niemiecki profesor, laureat medalu Fieldsa, opracował niezwykle skomplikowany wynik dotyczący tzw. przestrzeni kondensowanych. Dowód liczył setki stron i był tak abstrakcyjny, że tylko wąska grupa ekspertów potrafiła w ogóle go czytać.

Sam Scholze nie był pewien, czy w tym gąszczu nie ukrył się błąd. Zamiast prosić kolejnych kolegów o lekturę, postawił na ruch, który kilka lat temu brzmiałby jak science fiction: ogłosił otwarty projekt nazwany Liquid Tensor Experiment. Zaprosił matematyków i informatyków, którzy znają system Lean, aby przepisali jego dowód na język formalny zrozumiały dla komputera.

Asystent dowodów wymaga absolutnej precyzji. Nie uwierzy na słowo żadnemu autorytetowi, nawet nobliście matematyki.

W praktyce oznaczało to rozbicie skomplikowanego wyniku na tysiące małych kroków, z których każdy musiał zostać zrozumiany przez program i zatwierdzony jako logicznie poprawny. Po pół roku pracy międzynarodowy zespół ogłosił sukces: teoria Scholzego przeszła przez komputerowe sito. Maszyna przeanalizowała około 180 tysięcy linii kodu, nie znajdując żadnej luki.

Dla autora był to poziom pewności nieporównywalny z tradycyjną recenzją. Dla środowiska – sygnał, że oto zaczyna się nowa epoka, w której wielkie twierdzenia przestają wisieć w próżni i dostają cyfrowy, niezwykle solidny fundament.

Nowy model współpracy w miejsce samotnej pracy

Liquid Tensor Experiment pokazał też drugą zmianę: matematyka przestaje być sportem indywidualnym. W jednym projekcie może brać udział kilkadziesiąt osób rozsianych po całym globie. Każda pracuje nad małym fragmentem, a Lean scala to wszystko w jeden spójny dowód i na bieżąco weryfikuje poprawność.

• zespół może rozwijać różne części dowodu równolegle;
• konflikty i błędy wychodzą na jaw natychmiast;
• całość tworzy uporządkowaną bazę wiedzy, którą łatwo wykorzystać w kolejnych pracach.

Takiego trybu pracy nie da się wyobrazić wyłącznie przy użyciu maili, pdf-ów i ręcznych notatek. Asystent dowodów pełni rolę wspólnego „placu budowy”, na którym każdy klocek jest dokładnie opisany, sprawdzony i gotowy do ponownego użycia.

Gigantyczne projekty, które kiedyś były nie do udźwignięcia

Jednym z najbardziej spektakularnych przykładów tej zmiany jest praca Maryny Viazovskiej nad upakowaniem kul w ośmiu wymiarach. Chodzi o bardzo klasyczny problem: jak najgęściej poukładać kule, gdy zamiast znanej z życia trójwymiarowej przestrzeni działamy w znacznie większej liczbie wymiarów. Viazovska znalazła eleganckie rozwiązanie dla wymiaru 8, a potem również 24. Zyskała za to medal Fieldsa, ale za pięknem kryła się brutalna trudność techniczna: pełne ręczne sprawdzenie wszystkich szczegółów mogłoby zająć lata.

Grupa badaczy postanowiła więc przepisać jej dowód na formalny język Lean. W praktyce wymagało to rozbicia pojęć z analizy funkcjonalnej, geometrii i teorii liczb na zbiory ścisłych definicji, twierdzeń pośrednich i lem. Cały projekt trwał miesiącami, a efektem była kompletna, komputerowo zweryfikowana wersja dowodu dostępna jako kod na GitHubie.

Asystenty dowodów zmieniają „za duże, by je sprawdzić” w „trudne, ale wykonalne”. To inna skala odwagi badawczej.

Program nie rozwiązał problemu za matematyków – nie wymyślił strategii ani kluczowych idei. Zrobił coś innego: bez zmęczenia i dekoncentracji sprawdził, czy wszystkie drobne cegiełki są ułożone zgodnie z regułami logiki. Ludzki zespół dostał wiarygodne potwierdzenie, że nawet w najbardziej skomplikowanych fragmentach nic się nie rozjeżdża.

Rosnące biblioteki wiedzy – matematyczne „Lego” dla kolejnych pokoleń

Takie formalizacje nie giną w szufladzie. Trafiają do ogromnych bibliotek, takich jak Mathlib w ekosystemie Lean. To obecnie ponad milion linii definicji, twierdzeń i pomocniczych lem, które można ponownie wykorzystywać jak klocki Lego.

Dla młodych badaczy to ogromne ułatwienie. Zamiast startować z pustą kartką, mogą oprzeć się na gotowej, sprawdzonej infrastrukturze: strukturach algebraicznych, przestrzeniach topologicznych, klasycznych twierdzeniach analizy. Minimalizuje to ryzyko, że jakaś podstawowa definicja zawiera drobną usterkę, która popsuje późniejszy wynik.

Gdy komputer mówi „stop”: wykryte błędy w nagradzanych pracach

Asystenty dowodów pełnią jednak nie tylko rolę potwierdzającą. Zdarza się, że w czasie formalizacji opublikowanego, nagradzanego twierdzenia program zgłasza sprzeczność. W jednym z takich projektów Lean wyłapał błąd w etapie pośrednim ważnego wyniku. Autorzy artykułu byli zmuszeni napisać fragment na nowo, bo żadna nieprecyzyjna intuicja nie przejdzie przez surowy filtr logiki formalnej.

W ludzkiej recenzji często zakłada się, że pewne kroki „są jasne” albo „łatwe do uzupełnienia”. Komputer tak nie działa. Potrzebuje każdego detalu: wszystkich założeń, dokładnych zakresów obowiązywania twierdzeń, ścisłej postaci przekształceń. Jeśli czegoś brakuje, dowód się po prostu urywa.

Maszyna nie ma szacunku dla autorytetów. Ma szacunek wyłącznie dla reguł logiki.

Efekt uboczny jest zaskakująco pozytywny. Pojawia się presja, by pisać dowody tak, aby dało się je bez większych problemów sformalizować. To wymusza klarowność, rezygnację z niejasnych skrótów myślowych i dokładne opisywanie założeń. Długofalowo może to zmienić standardy publikacji naukowych w matematyce teoretycznej.

AI na pomoc: asystent dowodu staje się bardziej ludzki

Przez lata narzędzia takie jak Lean odstraszały wielu matematyków. Trzeba było znać nie tylko teorię, lecz także specyficzny język programowania i skomplikowaną składnię. Szybko rozwijająca się sztuczna inteligencja zaczyna ten próg obniżać.

Pojawiają się interfejsy, w których badacz pisze dowód w stylu przypominającym notatki z zeszytu, a model językowy podpowiada, jak przełożyć to na kod formalny. Program sugeruje odpowiednie lemmy z biblioteki, poprawia źle dobrane definicje, uzupełnia żmudne techniczne fragmenty. Matematycy dostają wrażenie pracy z bardzo cierpliwym korepetytorem, który nigdy nie traci uwagi.

• młodsi badacze szybciej uczą się formalnego stylu;
• eksperci mogą skupić się na ideach, a nie na składni;
• samo pisanie kodu staje się bardziej zbliżone do naturalnego języka matematycznego.

Dzięki temu rośnie liczba osób, które są w stanie włączyć się w formalne projekty. A im więcej użytkowników, tym szybciej rosną biblioteki takie jak Mathlib, co z kolei jeszcze bardziej zachęca do korzystania z tych narzędzi.

Co to w praktyce zmienia dla samej matematyki?

Najczęściej pojawia się pytanie: czy komputer zastąpi matematyków? Na razie odpowiedź brzmi: nie. Programy nie potrafią samodzielnie wybierać obiecujących kierunków badań ani wymyślać zupełnie nowych metod. Świetnie radzą sobie za to z tym, w czym człowiek bywa zawodny: z drobiazgową kontrolą szczegółów.

W praktyce może dojść do wyraźnego podziału ról:

• ludzie proponują nowe hipotezy, strategie, analogie między różnymi dziedzinami;
• maszyny testują wewnętrzną spójność, sprawdzają wiele wariantów definicji, wskazują dokładne miejsca, gdzie brakuje argumentu;
• wspólne projekty łączą intuicję z bezlitosną weryfikacją.

Ryzykiem jest zbyt duża wiara w kod: błąd w formalizacji może sprawić, że „dowód” zatwierdzony przez program będzie tak naprawdę nie tym, co autor miał na myśli. Dlatego doświadczeni badacze podkreślają, że formalna weryfikacja powinna iść w parze z tradycyjnym zrozumieniem idei. Kod ma odzwierciedlać myśl, a nie ją zastępować.

Z drugiej strony rośnie szansa na przełomy w bardzo technicznych obszarach, gdzie człowiek po prostu nie daje rady przetworzyć ilości szczegółów. Tam, gdzie dziś zniechęca nas wizja tysięcy stron rachunków, duet człowiek–komputer może otworzyć drogę do nowych teorii. Matematyka, zamiast zamykać się w wąskim gronie wtajemniczonych, zaczyna przypominać duży projekt inżynieryjny, w którym ważne miejsce mają zarówno twórcy koncepcji, jak i ci, którzy dbają o niezawodność każdego pojedynczego elementu.