ИИ помогает раскрыть открытия, скрытые в тетрадях Курта Гёделя
Финский логик Ян фон Плато с помощью ИИ-модели Claude изучил 16 тетрадей австрийского логика Курта Гёделя и обнаружил сотни ранее неизвестных теорем. Независимый профессор отмечает, что историки должны определить, какая часть результата принадлежит ИИ, а какая — самому Гёделю.
Финский логик Ян фон Плато (Jan von Plato), исследователь Хельсинкского университета, в сентябре использовал ИИ-модель Claude, чтобы разобраться в тетрадях, которые австрийский логик Курт Гёдель (Kurt Gödel) вёл в начале 1940-х годов. Оказалось, что Гёдель доказал сотни теорем, о которых никто не знал. Теоремы о неполноте, опубликованные Гёделем в 1931 году, преобразили математику и проложили путь цифровой эпохе, поэтому его неопубликованные работы интересуют историков науки.
Трудный материал
С 2017 года фон Плато руководит проектом по изучению 16 тетрадей, известных как «workbooks». В них 1009 страниц плотного текста о математике и логике, значительная часть которого написана немецкой стенографией Габельсбергера, устаревшей ещё при жизни Гёделя. Проект получил грант Европейского исследовательского совета в размере 2,5 млн евро. Фон Плато сам выучил эту стенографию и говорит, что в мире её читают лишь шесть человек. Поначалу работа шла очень медленно — примерно страница в неделю.
Что нашёл Claude
После встречи с специалистами по информатике на конференции во Франции фон Плато показал модели свои расшифровки, шесть собственных книг о Гёделе и другую научную литературу. Через пару дней он получил 650-страничное объяснение, которое пришлось проверять постранично.
Claude заключил, что в тетрадях есть почти полное доказательство независимости аксиомы выбора. В 1966 году, когда Пол Коэн (Paul Cohen) получил медаль Филдса за этот результат, Гёдель заявил, что доказал его ещё в 1940-х, но восстановить доказательство не смог. По словам фон Плато, не хватало лишь одного правильного определения. Восстановленное доказательство он проверил в системе проверки доказательств Coq, и оно прошло проверку.
Всего Claude выделил 663 теоремы. Около 400 подтвердились в исходной формулировке, примерно 200 потребовали исправления, около 50 оказались неверными. Фон Плато также утверждает, что в тетрадях есть 14 тем в логике, которые не исследовались.
Осторожная оценка
Джоэл Дэвид Хэмкинс (Joel David Hamkins), профессор логики Университета Нотр-Дам, реконструкцию не видел, но сказал, что, если она выдержит проверку, это замечательно и интересно с исторической точки зрения. По его словам, вопрос о том, какая доля принадлежит Claude, а какая Гёделю, — задача для историков, а сходство с доказательством Коэна не означает, что оно было у Гёделя.
