ИИ нашел в тетрадях Гёделя 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. Окончательное признание таких доказательств зависит от их проверки математическим сообществом.
