Notatniki Gödla: Claude znalazł w nich 663 twierdzenia

13 listopada „The Guardian” opisał, jak fiński logik Jan von Plato z Uniwersytetu Helsińskiego użył modelu Claude do analizy notatników Kurta Gödla z początku lat 40. Według von Plato Claude w kilka dni przygotował omówienie wszystkich 1009 stron i wskazał w nich 663 twierdzenia, w tym setki, o których nikt wcześniej nie wiedział.

Czym są notatniki Gödla?

Po twierdzeniach o niezupełności z 1931 r. Gödel opublikował już tylko kilka prac, ale zostawił dziesiątki tysięcy stron rękopisów. Wśród nich jest 16 zeszytów z początku lat 40. (tzw. „workbooks”), razem 1009 gęsto zapisanych stron o matematyce i logice. Dużą część Gödel zanotował stenografią Gabelsbergera, niemieckim systemem, który był przestarzały już wtedy, gdy po niego sięgał.

Von Plato zajmuje się zeszytami od 2017 r. Dostał na ten projekt 2,5 mln euro z Europejskiej Rady ds. Badań Naukowych (ERC), sam nauczył się stenografii Gabelsbergera i zebrał mały zespół. Zrozumienie matematycznej treści szło w tempie mniej więcej jednej strony na tydzień. Łatwo policzyć, że przy 1009 stronach oznacza to blisko dwadzieścia lat pracy.

Co zrobił Claude?

W sierpniu, na konferencji we Francji poświęconej AI i dowodzeniu twierdzeń, informatycy podsunęli von Plato pomysł, żeby spróbował z Claude’em. We wrześniu pokazał modelowi swoje transkrypcje zeszytów, sześć własnych książek o Gödlu i inną literaturę naukową.

Claude nie odczytywał więc stenografii. Pracował na tekście, który ludzie wcześniej przepisali, a jego zadaniem było to, co szło najwolniej, czyli ustalenie, co z tych zapisków matematycznie wynika.

Po kilku dniach von Plato miał 650-stronicowe objaśnienie całości. Jak mówi, trzeba je było kontrolować strona po stronie, ale człowiek takiej pracy nie wykona: czyta po jednej stronie, zapomina, a na 50 stron potrzebuje roku. Model natomiast widzi wszystkie pisma Gödla jako jedną całość (cytując „It can see all of Gödel’s writings as one piece”).

Potem von Plato poprosił o listę wszystkich twierdzeń, dla których Gödel miał dowód, szkic dowodu albo pomysł na dowód. Claude znalazł ich 663. Wyniki trafiły do Coq, programu sprawdzającego poprawność dowodów matematycznych:

1. około 400 twierdzeń przeszło weryfikację w zapisanej postaci,
2. około 200 trzeba było „naprawić”, czyli doprecyzować sformułowanie albo dodać założenie,
3. około 50 okazało się fałszywych.

Fałszywe twierdzenia von Plato tłumaczy tym, że Gödel, czytając ponownie własne notatki, sam dopisywał czasem na marginesie „falsch!” albo „schlecht!”.

Według niego w zeszytach są dziesiątki wyników, które świat poznał dopiero w latach 70. i 80., oraz 14 wątków w logice, których nikt dotąd nie podjął.

Czy Gödel wyprzedził Cohena?

W 1966 r. amerykański matematyk Paul Cohen dostał Medal Fieldsa za wykazanie niezależności hipotezy continuum i aksjomatu wyboru. Gödel zareagował stwierdzeniem, że ten wynik udowodnił już w latach 40. Kiedy koledzy poprosili o dowód, nie potrafił go odtworzyć z notatek.

Pierwsze zadanie, jakie dostał Claude, dotyczyło właśnie tej sprawy: czy w zeszytach jest dowód niezależności aksjomatu wyboru? Odpowiedź brzmiała „tak, prawie”. Według von Plato Gödlowi zabrakło jednego kroku, bo użył błędnej definicji, chociaż dwa lata wcześniej miał poprawną. Claude przedstawił zrekonstruowany dowód, a von Plato sprawdził go w Coq i dowód przeszedł weryfikację.

Joel David Hamkins, profesor logiki z Uniwersytetu Notre Dame, rekonstrukcji nie widział i jest ostrożniejszy. Jeśli dowód się obroni, będzie to jego zdaniem rzecz niezwykła i historycznie ciekawa, ale to, że w notatkach jest coś przypominającego dowód Cohena, nie znaczy, że Gödel ten dowód miał, tylko że był na dobrej drodze. Dodał też, że ustalenie, ile jest w tym Claude’a, a ile Gödla, to zadanie dla historyków (cytując „how much is Claude and how much is Gödel is a job for the historians”).

Na co zwrócić uwagę?

Po pierwsze, na źródło. Wszystkie liczby znamy z rozmowy von Plato z dziennikarzem. W artykule nie ma odnośnika do publikacji, listy twierdzeń ani plików Coq, więc na razie trudno cokolwiek sprawdzić samodzielnie.

Po drugie, na 200 „naprawionych” twierdzeń. Skoro trzeba było doprecyzować sformułowanie albo dodać założenie, to pytanie Hamkinsa wraca przy każdym z nich: czy to jeszcze wynik Gödla? Podobnie jest ze zrekonstruowanym dowodem niezależności aksjomatu wyboru, skoro w zeszytach z tego okresu Gödel użył błędnej definicji.

Po trzecie, na to, co potwierdza Coq. Program sprawdza, czy dowód jest poprawny. Nie rozstrzyga, czy Gödel ten dowód miał ani czy twierdzenie zapisane w Coq jest tym, o które Gödlowi chodziło. To już ocena ludzi, którzy znają rękopisy.

Czy to coś nowego w świecie AI?

W październiku pisałem o pracy OpenAI, według której model obalił hipotezę czasu wykładniczego, i o weryfikacji formalnej 123 bibliotek z Claude’em, a kilka dni temu o AlphaProof Code. We wszystkich tych przypadkach modele pisały nowe dowody.

Tutaj model czyta cudzą matematykę sprzed ponad 80 lat i szuka połączeń w tysiącu stron, których człowiek nie utrzyma w głowie naraz. Podział ról jest jednak ten sam: model proponuje, program do sprawdzania dowodów weryfikuje, a człowiek decyduje, co z tego wynika. A nieprzeczytanych archiwów jest więcej (sam Gödel zostawił dziesiątki tysięcy stron).

FAQ

Która wersja Claude’a analizowała notatniki Gödla?

Tego nie wiemy. W artykule mowa jest tylko o modelu AI Claude, bez wersji i bez informacji, z jakiego produktu korzystał von Plato.

Co dalej z rękopisami Gödla?

Von Plato zapowiada dalsze badania tych kilkunastu nowych wątków w logice, a po zakończeniu obecnych projektów chce zająć się notatnikami Gödla z fizyki i kosmologii, które nazywa nieznanym terytorium.