13 ноября The Guardian (заблокирован в РФ) рассказала о результатах проекта Хельсинкского университета по изучению неопубликованных рабочих тетрадей математика Курта Гёделя. Подключённая к проекту модель Claude выделила в записях 663 утверждения, для которых Гёдель оставил доказательство, его набросок или идею. Около 400 формализованных утверждений прошли проверку без изменений, примерно 200 потребовали уточнений, а около 50 оказались ложными.
Это не новый запуск Claude и не работа, выполненная моделью в одиночку. Финский логик Ян фон Плато руководит разбором архива с 2017 года, а Claude подключили в сентябре 2026-го. Исследователи уже расшифровали рукописи и передали модели транскрипции, шесть книг фон Плато о Гёделе и другую научную литературу.
Всего проект охватывает 16 тетрадей начала 1940-х годов, или 1009 страниц плотных записей по математике и логике. Значительная их часть написана немецкой стенографией Габельсбергера, которая считалась устаревшей ещё при жизни Гёделя. До привлечения Claude математическое изучение архива продвигалось примерно на одну страницу в неделю.
Читайте также
Модель составила 650-страничное объяснение содержимого тетрадей за несколько дней. По словам фон Плато, его всё равно необходимо проверять постранично. Главное ускорение состояло не в автоматическом доказательстве теорем, а в способности сопоставить фрагменты, разбросанные по тысяче страниц, и превратить их в перечень результатов для дальнейшей работы специалистов.
Для проверки исследователи использовали Coq, программный инструмент, в котором математические утверждения и доказательства записывают в формальной форме. Около 400 результатов были подтверждены в первоначальной формулировке. Примерно 200 удалось исправить, сделав утверждение точнее или добавив недостающее условие. Числа приблизительные и в публикации не складываются ровно в 663.
Около 50 утверждений оказались ложными. Из опубликованных данных нельзя заключить, на каком именно этапе возникла каждая ошибка: в исходных рассуждениях Гёделя, транскрипции, интерпретации Claude или последующей формализации. Поэтому результат не следует представлять как подсчёт «галлюцинаций» модели или как автоматическое опровержение Гёделя.
Отдельно команда реконструировала рассуждение о независимости аксиомы выбора. Гёдель утверждал, что получил такой результат ещё в 1940-х годах, но позднее не смог восстановить доказательство. Der Standard описывает нынешнюю работу как найденное ИИ «недостающее решение», однако подробный рассказ The Guardian осторожнее: в одной из записей Гёдель использовал неверное определение, хотя правильный вариант встречался в его более ранних заметках. Реконструированная версия прошла проверку в Coq, но это не означает, что в тетрадях уже содержалось полностью готовое и безошибочное доказательство.
Гёдель наиболее известен теоремами о неполноте 1931 года. В упрощённой формулировке они показывают, что в достаточно выразительной непротиворечивой формальной системе существуют утверждения, которые нельзя доказать средствами самой системы. После главных работ 1930-х годов математик публиковался редко, хотя его неопубликованный архив насчитывает десятки тысяч страниц.
Практическая ценность проекта заключается в разделении задач: языковая модель быстро строит карту большого неоднородного архива, а специалисты и формальная система проверяют конкретные математические выводы. Это перспективный сценарий для работы с рукописями и научной литературой, но пока не независимое доказательство надёжности Claude. В опубликованном описании не указаны точная версия модели, использованные запросы и полный набор формализаций, поэтому воспроизводимость результата ещё предстоит оценить.