Специалисты из Хельсинкского университета с помощью модели искусственного интеллекта Claude расшифровали рабочие тетради выдающегося логика XX века Курта Гёделя. В ходе исследования в записях были обнаружены сотни ранее неизвестных доказанных теорем, что подтверждает, что ученый значительно опережал свое время.
Объектом изучения стали 16 тетрадей, написанных в начале 1940-х годов, общим объемом 1009 страниц. Большая часть текста была составлена на Gabelsberger — немецкой стенографии, которая была устаревшей даже в эпоху Гёделя. До применения ИИ прогресс в изучении материалов был крайне медленным: исследователи могли разбирать примерно одну страницу в неделю.
Роль ИИ в расшифровке
Ян фон Плато, возглавляющий проект с 2017 года, предоставил модели Claude свои транскрипции тетрадей, шесть собственных книг о Гёделе и другую научную литературу. За несколько дней ИИ подготовил подробный разбор всего материала объемом 650 страниц. По словам фон Плато, человек не способен удерживать в памяти все взаимосвязи в таком объеме текста, в то время как ИИ видит все записи как единое целое.
В результате анализа Claude обнаружил 663 теоремы, для которых Гёдель либо привел доказательство, либо набросал его схему или идею. Для проверки этих данных использовалась программа Coq, предназначенная для верификации математических доказательств. Около 400 теорем были подтверждены в исходном виде, еще 200 удалось исправить путем уточнения формулировок, а около 50 оказались ошибочными.
Исторические открытия
Особое внимание уделили вопросу о независимости аксиомы выбора. В 1966 году за доказательство этого утверждения Пол Коэн получил Филдсовскую премию. Гёдель утверждал, что доказал это еще в 1940-х, но не смог восстановить решение из своих заметок. Анализ Claude показал, что Гёдель был в одном шаге от результата: он допустил одну ошибку в определении, хотя за два года до этого использовал верное.
Ян фон Плато отметил, что архитектура доказательства Гёделя выглядит «замечательно» и объединяет результаты теории множеств в единую систему. Он полагает, что если бы Гёдель опубликовал эту работу в 1940 году, он мог бы стать лауреатом Филдсовской премии.
Дальнейшие планы
По данным Claude, в тетрадях содержатся более десяти тем по логике и основаниям математики, которые не изучались на протяжении последних 80 лет. Кроме того, Ян фон Плато планирует приступить к изучению записей Гёделя по физике и космологии, которые остаются практически неисследованной территорией.
Профессор логики из Университета Нотр-Дам Джоэл Дэвид Хэмкинс отметил, что подобные находки исторически интересны, однако историкам предстоит определить, какая часть работы принадлежит самому Гёделю, а какая является результатом реконструкции ИИ.
