ИИ выявил в тетрадях Гёделя 663 математических утверждения

Нейросеть Claude содействовала ученым в обнаружении 663 математических утверждений в рукописях австрийского логика Курта Гёделя, включая как завершенные теоремы, так и черновики доказательств. Об этом сообщил руководитель проекта из Хельсинкского университета, финский математик Ян фон Плато, в интервью газете The Guardian. Об этом сообщает портал Life.ru.

Исследователи анализируют 16 рабочих тетрадей Гёделя, созданных в начале 1940-х годов. Эти тетради содержат 1009 страниц, посвященных математике и логике, причем большая часть текста написана устаревшей немецкой стенографией Габельсбергера. До использования ИИ ученые продвигались всего на одну страницу в неделю.

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

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

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

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

Ранее сообщалось, что OpenAI объявила о предложенном искусственным интеллектом решении одной из семи «задач тысячелетия» — проблемы Навье — Стокса. По данным компании, для поиска доказательства было задействовано множество ИИ-агентов, а формальная запись результата была представлена в системе Lean. Вопрос окончательного признания таких доказательств зависит от их проверки математическим сообществом.

Следите за актуальными событиями в режиме реального времени в разделе «Последние новости» на Life.ru.

Больше новостей и эксклюзивных видео смотрите в канале Самара Онлайн 24 в MAX

Читайте также: