Учёные Хельсинкского университета применили Claude для анализа архивных записей одного из величайших математиков XX века - Курта Гёделя. ИИ помог систематизировать 1009 страниц сложных рукописей и выделить 663 математических утверждения, многие из которых ранее оставались неизвестными исследователям. Однако последующая проверка показала, что далеко не все найденные результаты были правильными.
13 ноября 2026 года The Guardian рассказала о результатах проекта финского логика Яна фон Платона (Jan von Plato), который занимается изучением неопубликованных работ Гёделя с 2017 года.
Почему рукописи оставались нерасшифрованными
Курт Гёдель известен прежде всего теоремами о неполноте, опубликованными в 1931 году. Они показали принципиальные ограничения формальных математических систем и оказали огромное влияние на развитие математической логики и информатики.
При этом значительная часть исследований учёного так и осталась в рукописях.
Особый интерес представляют 16 рабочих тетрадей начала 1940-х годов. Они содержат 1009 страниц математических рассуждений, во многом записанных немецкой стенографией Габельсбергера - системой письма, которую сегодня способны читать лишь немногие специалисты.
Фон Платон получил грант Европейского исследовательского совета на 2,5 млн евро и собрал команду для изучения архива. Работа продвигалась медленно: исследователям удавалось подробно разбирать примерно одну страницу в неделю.
Что изменилось после подключения Claude
В сентябре 2026 года фон Платон начал использовать Claude, предоставив модели транскрипции рукописей, собственные научные книги и дополнительные материалы по математической логике.
За несколько дней ИИ подготовил примерно 650-страничное объяснение содержимого тетрадей.
Главное преимущество заключалось в возможности анализировать материалы как единое целое: сопоставлять определения, доказательства и идеи, встречающиеся в разных частях архива.
Исследователи попросили модель извлечь все утверждения, для которых Гёдель оставил полные доказательства, наброски доказательств или идеи.
Claude выделил 663 результата. Для проверки команда использовала Coq - систему формальной верификации математических доказательств.
По данным фон Платона:
- Около 400 утверждений удалось подтвердить в исходной формулировке.
- Примерно 200 потребовали уточнения условий или исправления формулировок.
- Около 50 оказались ошибочными.
Эти цифры особенно важны для оценки возможностей ИИ. Модель помогла найти и организовать материал, а достоверность математических утверждений проверялась отдельно.
Гёдель мог опередить одно из крупнейших открытий XX века
Самая интригующая находка связана с исследованиями независимости аксиомы выбора.
В 1960-х годах математик Пол Коэн разработал революционные методы теории множеств и получил Филдсовскую премию. Ещё при жизни Гёдель утверждал, что пришёл к похожим результатам гораздо раньше, однако не смог восстановить своё доказательство.
Анализ тетрадей обнаружил рассуждение, близкое к искомому доказательству. По словам фон Платона, в нём присутствовала одна неправильная дефиниция, хотя корректное определение Гёдель использовал в более ранних записях.
Исследователь смог проверить реконструированное доказательство с помощью Coq.
Впрочем, исторический приоритет из этого автоматически не следует. Найденные рукописи показывают направление мысли Гёделя, но вопрос о том, насколько завершённым было его открытие, остаётся предметом исследования.
Что говорят математики
Профессор математической логики Университета Нотр-Дама Джоэл Дэвид Хэмкинс (Joel David Hamkins) назвал потенциальную находку исторически значимой, но призвал к осторожности.
Хэмкинс подчеркнул, что сам не изучал реконструкцию доказательства. По его мнению, сходство с результатами Коэна ещё не означает, что Гёдель полностью получил такое же доказательство. Историкам математики предстоит разобраться, какая часть результата принадлежит автору рукописей и какую роль сыграла последующая реконструкция.
Сам фон Платон предполагает, что в тетрадях содержатся как минимум 14 направлений математической логики, которые оставались практически неизученными более восьмидесяти лет.
Часть большого научного тренда
ИИ всё активнее используется для поиска и проверки научных результатов. Например, исследовательские системы Google DeepMind помогают формализовать математические доказательства и проверять свойства программного обеспечения.
Особенность работы с архивом Гёделя состоит в сочетании исторического анализа, понимания сложной математической терминологии и машинной проверки доказательств.
Такой подход может оказаться полезным для изучения больших массивов архивных документов, рукописных научных работ и забытых исследований.
Главный вывод: Claude значительно ускорил научную работу, на которую раньше уходили годы. Но история одновременно показывает ограничения языковых моделей: даже при обнаружении сотен перспективных утверждений часть из них оказалась ошибочной. Надёжный научный результат потребовал участия специалистов и формальной верификации.
Источники: