Claude pomaga helsińskiemu logikowi odczytać skrótowe zeszyty robocze Gödla i odkryć setki twierdzeń

The Guardian donosi, że Jan von Plato, który od 2017 roku kieruje projektem Uniwersytetu Helsińskiego poświęconym 16 wczesnym „zeszytom roboczym” Kurta Gödla z początku lat 40. (1009 stron, z czego znaczna część zapisana jest przestarzałym stenograficznym pismem Gabelsbergera), we wrześniu przekazał Claude’owi swoje transkrypcje, wcześniejsze książki o Gödelu oraz literaturę przedmiotu. Według von Plato w ciągu kilku dni Claude przygotował 650-stronicowe objaśnienie zeszytów, które — jak mówi — trzeba było sprawdzać strona po stronie.

Co, jak twierdzi von Plato, udało się znaleźć. Zapytany, czy zeszyty zawierają dowód niezależności aksjomatu wyboru, Claude odtworzył dowód, który według von Plato jest „niemal” kompletny, ale zawiera jedną błędną definicję — poprawną u Gödla już dwa lata wcześniej. Von Plato mówi, że odtworzony dowód przeszedł weryfikację za pomocą asystenta dowodów Coq. Poproszony o wypisanie wszystkich twierdzeń, które Gödel udowodnił, naszkicował lub których dowód rozważał, Claude wymienił 663. Von Plato twierdzi, że około 400 zweryfikowano w Coq w podanej postaci, około 200 wymagało poprawek, a około 50 było fałszywych. Mówi też, że Claude wskazał ponad tuzin zagadnień z logiki, którymi dotąd się nie zajęto.

Zastrzeżenia. Joel David Hamkins z University of Notre Dame, który nie widział rekonstrukcji, powiedział The Guardian, że jeśli się ona obroni, będzie „niezwykła i interesująca z historycznego punktu widzenia”, ale ustalenie, jaka część należy do Claude’a, a jaka do Gödla, jest zadaniem dla historyków. Dodał też, że podobieństwo do dowodu Cohena nie oznacza, iż Gödel go znał.