Dowody z obwodów

To oczywiste! – ktoś odpowie. – W matematyce nie chodzi przecież jedynie o liczby i rachunki. Czy w muzyce chodzi wyłącznie o nuty? Czy ma sens mówienie, że architekci zajmują się cegłami? Matematyka to nauka o abstrakcyjnych, formalnych strukturach, a systemy liczbowe to li tylko przykłady takich struktur”. Wszystko prawda. Sednem pracy matematyka nie są równania, które trzeba rozwiązać, lecz twierdzenia, które trzeba udowodnić.

Czymże jednak jest dowód twierdzenia? To sposób przejścia od wyjściowych założeń do końcowej tezy w pewnej skończonej liczbie kroków, polegających na stosowaniu przyjętych aksjomatów, praw logiki oraz innych, wcześniej udowodnionych twierdzeń. Wychodząc od tego spostrzeżenia, wybitny niemiecki matematyk David Hilbert stwierdził na początku XX w., że matematyka jest swego rodzaju grą, w której pionkami są symbole, a regułami – logika i aksjomaty. Choć dziś wiemy, że wizja Hilberta nie jest prawdziwa w odniesieniu do całej matematyki (więcej na ten temat za chwilę), to wciąż można zasadnie pytać, czy da się wyszkolić sztuczną inteligencję, by odkrywała nowe prawdy matematyczne, tak jak potrafi odkrywać nowe strategie w szachach albo w go. Pełnej odpowiedzi jak dotąd nie znamy. Ale nawet to, co już wiemy, jest fascynujące.

Obliczenia wspomagane

Zastosowanie komputerów w dowodzeniu twierdzeń matematycznych dzieli się na kilka typów. Istnieją tzw. dowody wspomagane komputerowo (computer- -assisted proofs), polegające na tym, że specjalnie zaprojektowany algorytm wykonuje obliczeniową czarną robotę, której nie podołałaby nawet armia rachmistrzów. Najbardziej znanym reprezentantem tej grupy jest dowód tzw. twierdzenia o czterech barwach z roku 1976, które w uproszczeniu głosi, że każdą mapę polityczną da się pokolorować przy użyciu zaledwie czterech kolorów tak, by sąsiadujące państwa były różnokolorowe. Innym przykładem jest dowód tzw. hipotezy Keplera dotyczącej optymalnego upakowania kul w przestrzeni, przeprowadzony w 1998 r., niemal 400 lat po jej postawieniu przez słynnego astronoma.

Innym zastosowaniem jest zautomatyzowane sprawdzanie dowodów (auto- mated proof checking). Wymaga ono zapisania badanego dowodu w specjalnym, sformalizowanym języku, którym posługuje się komputerowy „kontroler jakości”, tzw. proof checker. Ten ostatni zajmuje się już całą resztą, wynajdując ewentualne luki lub logiczne potknięcia. Choć zdawanie się na werdykt automatów w kwestii poprawności rozumowania nie jest obecnie powszechną praktyką, było ono kluczowe w ostatecznym zaakceptowaniu dwóch wspomnianych wyżej dowodów wspomaganych komputerowo.

Ale dlaczego właściwie zautomatyzowana weryfikacja dowodów nie jest powszechną praktyką w pracy matematyków. Przecież oszczędziłoby to mnóstwo czasu (nie wspominając o nerwach) autorom i recenzentom artykułów naukowych! Problemem okazuje się niestety przekład ludzkiej matematycznej prozy na zapis zrozumiały dla proof checkera, który bardziej przypomina gęsty, programistyczny kod niż język naturalny.

Najdalej w dziedzinie tłumaczenia żargonu matematyków na język maszyn dotarł projekt Mizar, zapoczątkowany ponad 40 lat temu przez nieżyjącego już dr. Andrzeja Trybulca i wciąż rozwijany na Uniwersytecie w Białymstoku (we współpracy z ośrodkami kanadyjskim i japońskim), który może pochwalić się korpusem niemal 60 tys. sformalizowanych i automatycznie sprawdzonych dowodów twierdzeń.

Biblioteka Matematyczna Mizara (Mizar Mathematical Library, MML), choć imponująca, pokrywa jednak stosunkowo niewielką część matematyki i to głównie na poziomie studiów licencjackich. Przy obecnym tempie prac dotarcie w pobliże frontu matematycznych badań wymagać będzie wielu dekad wytężonej transkrypcji.

Twierdzenia na żądanie

Rozwiązaniem – istnym deus ex machina – byłoby włączenie do Mizara algorytmów, które nie tylko sprawdzają, ale przede wszystkim wynajdują dowody znanych, a najlepiej również nieznanych twierdzeń. Zajmuje się tym dziedzina badań nad sztuczną inteligencją znana jako zautomatyzowane dowodzenie twierdzeń (automated theorem proving, ATP), która odniosła już pierwsze sukcesy. Przykładowo, obecnie ok. 59 proc. rezultatów figurujących w MML udało się niezależnie udowodnić za pomocą różnych technik AI (od niedawna zajmuje się tym m.in. firma DeepMind, której program AlphaGo trzy lata temu osiągnął poziom mistrzowski w go). Z kolei już w 1996 r. metodami ATP udowodniono tzw. hipotezę Robbinsa – dość ezoteryczny problem z teorii tzw. algebr Boole’a, z którym od 60 lat bezskutecznie zmagało się wielu znakomitych matematyków i logików, w tym sam Alfred Tarski.

Co ciekawe, algorytmy ATP wykroczyły poza czystą matematykę – z ich usług korzysta się przy projektowaniu procesorów oraz testowaniu i optymalizacji oprogramowania. Jednak na chyba najbardziej nietypowy pomysł wpadł szkocki start-up TheoryMine, założony przez pracowników Uniwersytetu Edynburskiego. Ich algorytm generuje na żądanie nowe twierdzenie z algebry abstrakcyjnej, które klient może nazwać wybranym przez siebie imieniem, otrzymując gustowny elektroniczny certyfikat – to wszystko w cenie 15 funtów. W odróżnieniu od podobnych ofert nadawania imion gwiazdom lub kupna działki na Marsie, TheoryMine załącza rygorystyczny dowód, że nowe twierdzenie jest prawdziwe.

Ale żarty na bok. Czy postępy sztucznej inteligencji na polu ATP oraz w dziedzinie przetwarzania języka naturalnego (który pozwoliłby algorytmom uczyć się bezpośrednio z podręczników i artykułów, z pominięciem MML i podobnych baz) doprowadzą w przyszłości do zastąpienia białkowych matematyków krzemowymi? Zdania na ten temat są podzielone.

Jednymi z czołowych wątpiących w nadejście cyfrowych Gaussów i Banachów są filozof John Lucas oraz fizyk matematyczny Roger Penrose. Uczeni ci zwracają uwagę na pewne fundamentalne ograniczenia wszelkich systemów formalnych i bazujących na nich algorytmów, odkryte w 1930 r. przez logika Kurta Gödla. Udowodnił on (sic!), iż w każdym takim systemie albo tkwią sprzeczności, albo zawiera on zdania prawdziwe, ale niedające się w jego ramach udowodnić. Więcej nawet, Gödlowi udało się skonstruować takie zawiłe, samoodnoszące się zdanie, którego nie da się logicznie wywieść z aksjomatów systemu, ale którego prawdziwość można dostrzec, pojmując jego znaczenie. To właśnie w ten sposób upadła Hilbertowska wizja matematyki jako czysto syntaktycznej gry symboli pozbawionych treści. I to właśnie dlatego, zgodnie z argumentem Lucasa-Penrose’a, umysł matematyka zasadniczo nie daje się zastąpić algorytmem – ten ostatni, choćby nawet taśmowo produkował nowe twierdzenia wraz z dowodami, będzie bezradny w obliczu zdań typu gödlowskiego.

Z drugiej strony, zdania tego typu niezmiernie rzadko pojawiają się w praktyce badawczej. Nawet jeśli leżą poza zasięgiem przyszłej AI, pracy dla niej nie zabraknie. Co do tego, że taka AI powstanie, nie ma wątpliwości Timothy Gowers, matematyk i zdobywca Medalu Fieldsa, który obecnie pracuje nad nauczeniem algorytmów ATP języka naturalnego, w którym prezentowałyby swoje wyniki. Zapytany w 2013 r., kiedy spodziewa się nadejścia „sztucznych matematyków” dorównujących ludziom, oszacował, że na 50 proc. nastąpi to w ciągu 40 lat, a na 90 proc. do końca wieku. Gowers dodaje przy tym, że „sztuczni uczeni” reprezentujący inne nauki ścisłe i inżynieryjne nadejdą wkrótce potem.

Czy jako matematyk obawiam się takiej przyszłości? Raczej nie, choć niewątpliwie sposób uprawiania nauki uległby wówczas głębokim przeobrażeniom. Przeciwnie, byłbym podekscytowany mogąc, niczym w „Golemie XIV” Lema, słuchać wykładów sztucznej superinteligencji na temat jej nowych, głębokich wyników matematycznych.

Zakładając oczywiście, że w odróżnieniu od Lemowskiego superkomputera taka AI widziałaby we mnie godnego słuchacza. ©