Опередил науку на десятилетия: ИИ нашёл у Гёделя сотни забытых математических идей

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

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

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

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

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

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

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

Больше актуальных событий в режиме реального времени — читайте в разделе «Последние новости» на Life.ru.