ИИ помог раскрыть открытия в тетрадях Курта Гёделя — математика, опередившего своё время

Тетради, которые не удавалось прочитать

Курт Гёдель был одним из самых оригинальных мыслителей XX века. Его две теоремы о неполноте, опубликованные в 1931 году, изменили математику и помогли подготовить почву для цифровой эпохи. Они показывают, что в любой математической системе есть истинные утверждения, которые внутри этой системы нельзя ни доказать, ни опровергнуть. Эти результаты обозначили пределы математического знания, но также направили логику в новые области. В частности, они вдохновили Алана Тьюринга на работу 1936 года, положившую начало теории современных вычислений.

После работ 1930-х годов Гёдель опубликовал лишь несколько статей. При этом его неопубликованные материалы занимают десятки тысяч страниц и представляют большой интерес для историков науки.

С 2017 года Ян фон Плато руководит в Хельсинкском университете проектом по изучению 16 тетрадей, которые Гёдель вёл в начале 1940-х. Эти так называемые рабочие тетради насчитывают 1009 страниц плотных записей по математике и логике. Значительная часть написана стенографией Габельсбергера — немецкой системой записи, уже устаревшей при жизни Гёделя.

Фон Плато начал проект, когда ему предстоял обязательный выход на пенсию из университета. Он решил заняться загадочными стенографическими записями Гёделя, получил грант Европейского исследовательского совета на €2,5 млн (£2,1 млн), сам освоил Габельсбергера и собрал небольшую команду. По его словам, в мире эту стенографию умеют читать лишь шесть человек.

Альберт Эйнштейн вручает Курту Гёделю (второй справа) награду в Принстонском университете, где они подружились

Источник: theguardian.com

До привлечения Claude команда разбирала примерно одну страницу в неделю. В августе на конференции во Франции, посвящённой ИИ и доказательству теорем, фон Плато встретил специалистов по информатике, предложивших попробовать Claude. Вернувшись в Хельсинки, он передал модели собственные расшифровки тетрадей, а также шесть своих книг о Гёделе и другую научную литературу по теме.

Через несколько дней Claude подготовил 650-страничное объяснение записей. Фон Плато проверял его постранично. Он пояснил, что человеку трудно удерживать в памяти весь материал: обычно исследователи читают по одной странице и забывают детали, а на 50 страниц уходит около года. Claude смог связать сведения из тысячи страниц и рассматривать работы Гёделя как единое целое.

След независимого доказательства

Одним из первых заданий для Claude было выяснить, содержат ли тетради доказательство независимости аксиомы выбора. Это могло бы подтвердить заявление Гёделя, сделанное в 1966 году: он говорил, что получил соответствующий результат ещё в 1940-х.

Американский математик Пол Коэн получил в 1966 году Филдсовскую медаль — высшую награду в математике — за доказательство независимости двух известных утверждений: континуум-гипотезы и аксиомы выбора. Гёдель утверждал, что уже доказал этот результат в 1940-х, но, когда коллеги попросили его показать доказательство, он не смог восстановить его по записям.

Claude обнаружил в тетрадях почти готовое доказательство. По словам фон Плато, в одном определении Гёдель ошибся, хотя за два года до этого использовал верный вариант. Фон Плато считает, что, продолжи Гёдель работу ещё несколько месяцев, он мог бы прийти к правильному определению. Исследователь также отметил, что доказательство связывает результаты теории множеств в единую последовательность.

Фон Плато проверил восстановленное доказательство с помощью Coq — программы для проверки математических доказательств. Оно прошло проверку. По мнению исследователя, если бы Гёдель опубликовал работу об аксиоме выбора, он мог бы получить Филдсовскую медаль 1940 года. Фон Плато предположил, что Гёдель мог особенно остро воспринять награждение Коэна как упущенную возможность.

Микрофильм с примером стенографии Гёделя из одной из его записных книжек

Источник: theguardian.com

Что ещё нашли в записях

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

В тетрадях обнаружились более десятка тем по логике и основаниям математики, которые, по оценке Claude, не изучались в течение более чем 80 лет после того, как Гёдель их записал. Фон Плато планирует продолжить исследование рукописей, а после завершения текущих проектов по логике обратиться к тетрадям Гёделя по физике и космологии.

Историческая оценка

Джоэл Дэвид Хэмкинс, профессор логики в Университете Нотр-Дам в штате Индиана, не видел восстановленного Claude доказательства независимости аксиомы выбора. Он сказал, что, если доказательство выдержит проверку, это будет примечательно и важно для истории, но исследователям ещё предстоит определить вклад Claude и вклад самого Гёделя.

По словам Хэмкинса, сходство записей с доказательством Коэна само по себе не означает, что Гёдель уже располагал готовым результатом: оно показывает, что тот двигался в этом направлении. Хэмкинс добавил, что учёным не засчитывают работу, о которой они никому не сообщили, однако множество новаторских идей Гёделя делает содержательные находки в его тетрадях неудивительными.

По оценке Dataist, Claude здесь выступил инструментом для поиска связей в большом архиве, но математическую ценность результатов проверяли отдельно — в том числе с помощью Coq. Исторический вывод остаётся осторожным: найденные записи показывают, как далеко продвинулся Гёдель, но не отменяют вопроса о том, что именно он успел доказать и сообщить другим.