ИИ Claude нашёл в тетрадях Гёделя сотни неизвестных доказанных теорем

Финский логик из Хельсинкского университета Ян фон Плато с помощью ИИ-модели Claude, разработанной компанией Anthropic, разобрал 16 тетрадей австрийского логика Курта Гёделя, так называемые «рабочие тетради». Гёдель вёл их в начале 1940-х годов. Анализ показал, что он доказал сотни теорем, о которых прежде не было известно. Находка важна для истории математики: теоремы Гёделя о неполноте, опубликованные в 1931 году, изменили эту науку и подготовили почву для цифровой эпохи.

Трудный материал

После первых знаменитых результатов Гёдель опубликовал лишь несколько работ, но его неопубликованные записи занимают десятки тысяч страниц. С 2017 года фон Плато руководит проектом по изучению тетрадей, в которых 1009 плотно исписанных страниц по математике и логике. Значительная часть текста написана немецкой стенографией Габельсбергера, которая уже во времена Гёделя была устаревшей. Проект финансируется грантом Европейского исследовательского совета в 2,5 млн евро; фон Плато сам выучил эту стенографию и собрал небольшую команду. Работа шла медленно, примерно по странице в неделю.

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

Результаты

Фон Плато попросил модель выделить все теоремы, для которых у Гёделя было доказательство, набросок или идея доказательства. Claude нашёл 663. При проверке в Coq, программе для проверки математических доказательств, около 400 подтвердились в исходной формулировке, около 200 потребовали исправлений, примерно 50 оказались ложными. По словам фон Плато, в тетрадях есть и 14 тем в логике, которые не получили развития, а также результаты, до которых другие исследователи дошли лишь в 1970–1980-х годах.

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

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