ИИ обнаружил в тетрадях Гёделя 663 математических утверждений
Нейросеть Claude помогла ученым выявить в рукописях австрийского логика Курта Гёделя 663 математических утверждений, включая как готовые теоремы, так и наброски доказательств. О результатах анализа ранее неопубликованных работ сообщил газете The Guardian руководитель проекта из Хельсинкского университета, финский математик Ян фон Плато. Сообщает Life.ru.
Исследователи изучают 16 рабочих тетрадей Гёделя, созданных в начале 1940-х годов. В этих тетрадях содержится 1009 страниц по математике и логике, значительная часть текста написана устаревшей немецкой стенографией Габельсбергера. До использования ИИ ученые продвигались примерно на одну страницу в неделю.
Фон Плато предоставил Claude уже подготовленные расшифровки, свои книги о Гёделе и другую научную литературу. За несколько дней модель составила 650-страничный анализ рукописей и помогла связать разрозненные идеи. Полученные результаты затем проверялись постранично.
Из 663 найденных утверждений около 400 прошли формальную проверку в системе Coq без изменений. Примерно 200 потребовали уточнений или дополнительных условий, а около 50 оказались ошибочными. По словам фон Плато, в тетрадях были обнаружены идеи, предвосхитившие результаты 1970–1980-х годов, а также 14 направлений логики, которые почти не развивались. «Гёдель значительно опередил своё время», — отметил исследователь.
Особый интерес вызвали записи об аксиоме выбора. В 1966 году американский математик Пол Коэн получил Филдсовскую медаль за исследования независимости аксиомы выбора и континуум-гипотезы. Гёдель тогда утверждал, что пришёл к аналогичному результату раньше, но восстановить своё доказательство не смог.
Claude помог восстановить почти завершённое рассуждение Гёделя: в нём оказалось ошибочным одно определение, хотя правильный вариант встречался в более ранних записях. Восстановленное доказательство прошло проверку в Coq. Однако профессор логики Университета Нотр-Дам Джоэл Дэвид Хэмкинс подчеркнул, что сходство с последующим доказательством Коэна не означает, что Гёдель полностью завершил свою работу.
Ранее Life.ru сообщал, что OpenAI представила решение одной из семи «задач тысячелетия» — проблемы Навье — Стокса, предложенное искусственным интеллектом. По информации компании, для поиска доказательства использовали тысячи ИИ-агентов, а формальную запись результата представили в системе Lean. Вопрос окончательного признания таких доказательств зависит от их проверки математическим сообществом.
