Claude помогает гельсинкскому логику разобраться в стенографических рабочих тетрадях Гёделя и обнаружить сотни теорем

Как сообщает The Guardian, Ян фон Плато, возглавляющий с 2017 года проект Хельсинкского университета по изучению 16 ранних «рабочих тетрадей» Курта Гёделя начала 1940-х годов (1 009 страниц, значительная часть записана устаревшей стенографией Габельсбергера), в сентябре передал Claude свои расшифровки, прежние книги о Гёделе и научную литературу по теме. По словам фон Плато, за пару дней Claude подготовил 650-страничное объяснение тетрадей; он говорит, что его пришлось проверять страница за страницей.

Что, по словам фон Плато, удалось обнаружить. На вопрос, содержат ли тетради доказательство независимости аксиомы выбора, Claude восстановил доказательство, которое фон Плато назвал «почти» завершённым, — с одним неверным определением, хотя двумя годами ранее Гёдель использовал правильное. Фон Плато говорит, что восстановленное доказательство прошло проверку в системе Coq. На просьбу извлечь все теоремы, которые Гёдель доказал, наметил или задумал, Claude перечислил 663. По словам фон Плато, около 400 были подтверждены в Coq в сформулированном виде, около 200 требовали исправлений, а около 50 оказались ложными. Он также говорит, что Claude выявил более дюжины тем в логике, которые ещё не исследовались.

Оговорки. Джоэл Дэвид Хэмкинс из Университета Нотр-Дам, не видевший восстановленного доказательства, сказал The Guardian: если оно выдержит проверку, это будет «замечательным и исторически интересным» результатом. Однако, по его словам, вопрос о том, какая часть принадлежит Claude, а какая — Гёделю, должны решать историки; кроме того, сходство с доказательством Коэна не означает, что Гёдель располагал этим доказательством.