13 ноября 2026 г.
Claude разобрал записи Гёделя: около 400 результатов прошли проверку в Coq
По словам историка логики Яна фон Плато, около 400 результатов из записей Гёделя прошли проверку в Coq без изменений.
24 сентября 2026 года Ян фон Плато загрузил в Claude сотни страниц своих английских транскрипций записей Курта Гёделя и попросил разобрать аргументы.
Сначала была расшифровка. Гёдель оставил 1009 страниц рабочих тетрадей, во многом написанных устаревшей стенографией. Claude получил уже подготовленный английский текст. После теорем о неполноте 1931 года Гёдель публиковал мало работ, а его неопубликованное наследие насчитывает десятки тысяч страниц.
Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.
В интервью Der Standard от 19 октября фон Плато рассказал, что после нескольких промптов Claude построил по записям 1940–1942 годов доказательство независимости аксиомы выбора. По его словам, модель восстановила иной путь, чем тот, которым позднее пошёл Пол Коэн.
Проверяли отдельные результаты. По данным Guardian от 13 ноября, Claude выделил 663 результата. Фон Плато сообщил, что около 400 прошли проверку в системе формальных доказательств Coq без изменений. Около 200 потребовали исправлений, около 50 оказались ложными.
В тезисах октябрьского доклада фон Плато оценил объём подготовленных ИИ объяснений рабочих тетрадей примерно в 500 страниц и сообщил о проверке части доказательств в Coq.
Запись доклада фон Плато «Understanding Gödel in an Age of Machine Intelligence» от 19 октября доступна на YouTube.
Первоисточник